{- |
Module      :  ./CoCASL/StatAna.hs
Description :  static analysis for CoCASL
Copyright   :  (c) Till Mossakowski, Uni Bremen 2004-2005
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  hausmann@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

static analysis for CoCASL
-}

module CoCASL.StatAna where

import CoCASL.AS_CoCASL
import CoCASL.Print_AS ()
import CoCASL.CoCASLSign

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

import Common.AS_Annotation
import Common.GlobalAnnotations
import qualified Data.Set as Set
import qualified Common.Lib.Rel as Rel
import Common.Lib.State
import Common.Id
import Common.Result
import Common.DocUtils
import Common.ExtSign

import Control.Monad

import Data.Maybe
import Data.List (partition)

type CSign = Sign C_FORMULA CoCASLSign

instance TermExtension C_FORMULA where
    freeVarsOfExt :: Sign C_FORMULA e -> C_FORMULA -> VarSet
freeVarsOfExt sign :: Sign C_FORMULA e
sign cf :: C_FORMULA
cf = case C_FORMULA
cf of
       BoxOrDiamond _ _ f :: FORMULA C_FORMULA
f _ -> Sign C_FORMULA e -> FORMULA C_FORMULA -> VarSet
forall f e. TermExtension f => Sign f e -> FORMULA f -> VarSet
freeVars Sign C_FORMULA e
sign FORMULA C_FORMULA
f
       _ -> VarSet
forall a. Set a
Set.empty

basicCoCASLAnalysis
  :: (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA,
      Sign C_FORMULA CoCASLSign, GlobalAnnos)
  -> Result (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA,
             ExtSign (Sign C_FORMULA CoCASLSign) Symbol,
             [Named (FORMULA C_FORMULA)])
basicCoCASLAnalysis :: (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA,
 Sign C_FORMULA CoCASLSign, GlobalAnnos)
-> Result
     (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA,
      ExtSign (Sign C_FORMULA CoCASLSign) Symbol,
      [Named (FORMULA C_FORMULA)])
basicCoCASLAnalysis =
    Min C_FORMULA CoCASLSign
-> Ana C_BASIC_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
-> Ana C_SIG_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
-> Mix C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
-> (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA,
    Sign C_FORMULA CoCASLSign, GlobalAnnos)
-> Result
     (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA,
      ExtSign (Sign C_FORMULA CoCASLSign) Symbol,
      [Named (FORMULA C_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 C_FORMULA CoCASLSign
minExpForm Ana C_BASIC_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
ana_C_BASIC_ITEM Ana C_SIG_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
ana_C_SIG_ITEM Mix C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
ana_CMix

-- analyses cocasl sentences only
co_sen_analysis ::
        (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA, CSign, FORMULA C_FORMULA)
        -> Result (FORMULA C_FORMULA)
co_sen_analysis :: (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA,
 Sign C_FORMULA CoCASLSign, FORMULA C_FORMULA)
-> Result (FORMULA C_FORMULA)
co_sen_analysis (bs :: BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA
bs, s :: Sign C_FORMULA CoCASLSign
s, f :: FORMULA C_FORMULA
f) = let
                        mix :: Mix b s f e
mix = Mix b s f e
forall b s f e. Mix b s f e
emptyMix
                        allIds :: IdSets
allIds = [IdSets] -> IdSets
unite ([IdSets] -> IdSets) -> [IdSets] -> IdSets
forall a b. (a -> b) -> a -> b
$
                                (C_BASIC_ITEM -> IdSets)
-> (C_SIG_ITEM -> IdSets)
-> BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA
-> IdSets
forall b s f.
(b -> IdSets) -> (s -> IdSets) -> BASIC_SPEC b s f -> IdSets
ids_BASIC_SPEC (Mix C_BASIC_ITEM Any Any Any -> C_BASIC_ITEM -> IdSets
forall b s f e. Mix b s f e -> b -> IdSets
getBaseIds Mix C_BASIC_ITEM Any Any Any
forall b s f e. Mix b s f e
mix) (Mix Any C_SIG_ITEM Any Any -> C_SIG_ITEM -> IdSets
forall b s f e. Mix b s f e -> s -> IdSets
getSigIds Mix Any C_SIG_ITEM Any Any
forall b s f e. Mix b s f e
mix) BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA
bs
                                IdSets -> [IdSets] -> [IdSets]
forall a. a -> [a] -> [a]
: Mix Any Any Any CoCASLSign -> CoCASLSign -> IdSets
forall b s f e. Mix b s f e -> e -> IdSets
getExtIds Mix Any Any Any CoCASLSign
forall b s f e. Mix b s f e
mix (Sign C_FORMULA CoCASLSign -> CoCASLSign
forall f e. Sign f e -> e
extendedInfo Sign C_FORMULA CoCASLSign
s) IdSets -> [IdSets] -> [IdSets]
forall a. a -> [a] -> [a]
:
                                [Set SORT -> Set SORT -> Set SORT -> IdSets
mkIdSets (Sign C_FORMULA CoCASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
allConstIds Sign C_FORMULA CoCASLSign
s) (Sign C_FORMULA CoCASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
allOpIds Sign C_FORMULA CoCASLSign
s)
                                (Set SORT -> IdSets) -> Set SORT -> IdSets
forall a b. (a -> b) -> a -> b
$ Sign C_FORMULA CoCASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
allPredIds Sign C_FORMULA CoCASLSign
s]
                        mix' :: Mix b s f e
mix' = Mix b s f e
forall b s f e. Mix b s f e
mix { mixRules :: (TokRules, Rules)
mixRules = GlobalAnnos -> IdSets -> (TokRules, Rules)
makeRules GlobalAnnos
emptyGlobalAnnos IdSets
allIds}
                        in ((FORMULA C_FORMULA, FORMULA C_FORMULA) -> FORMULA C_FORMULA)
-> Result (FORMULA C_FORMULA, FORMULA C_FORMULA)
-> Result (FORMULA C_FORMULA)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (FORMULA C_FORMULA, FORMULA C_FORMULA) -> FORMULA C_FORMULA
forall a b. (a, b) -> a
fst (Result (FORMULA C_FORMULA, FORMULA C_FORMULA)
 -> Result (FORMULA C_FORMULA))
-> Result (FORMULA C_FORMULA, FORMULA C_FORMULA)
-> Result (FORMULA C_FORMULA)
forall a b. (a -> b) -> a -> b
$ Min C_FORMULA CoCASLSign
-> Mix Any Any C_FORMULA CoCASLSign
-> Sign C_FORMULA CoCASLSign
-> FORMULA C_FORMULA
-> Result (FORMULA C_FORMULA, FORMULA C_FORMULA)
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Mix b s f e
-> Sign f e
-> FORMULA f
-> Result (FORMULA f, FORMULA f)
anaForm Min C_FORMULA CoCASLSign
minExpForm Mix Any Any C_FORMULA CoCASLSign
forall b s f e. Mix b s f e
mix' Sign C_FORMULA CoCASLSign
s FORMULA C_FORMULA
f


ana_CMix :: Mix C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
ana_CMix :: Mix C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
ana_CMix = Mix Any Any Any Any
forall b s f e. Mix b s f e
emptyMix
    { getBaseIds :: C_BASIC_ITEM -> IdSets
getBaseIds = C_BASIC_ITEM -> IdSets
ids_C_BASIC_ITEM
    , getSigIds :: C_SIG_ITEM -> IdSets
getSigIds = C_SIG_ITEM -> IdSets
ids_C_SIG_ITEM
    , getExtIds :: CoCASLSign -> IdSets
getExtIds = \ e :: CoCASLSign
e -> let c :: OpMap
c = CoCASLSign -> OpMap
constructors CoCASLSign
e in
        Set SORT -> Set SORT -> Set SORT -> IdSets
mkIdSets (OpMap -> Set SORT
opMapConsts OpMap
c) (OpMap -> Set SORT
nonConsts OpMap
c) Set SORT
forall a. Set a
Set.empty
    , putParen :: C_FORMULA -> C_FORMULA
putParen = C_FORMULA -> C_FORMULA
mapC_FORMULA
    , mixResolve :: MixResolve C_FORMULA
mixResolve = MixResolve C_FORMULA
resolveC_FORMULA
    }

ids_C_BASIC_ITEM :: C_BASIC_ITEM -> IdSets
ids_C_BASIC_ITEM :: C_BASIC_ITEM -> IdSets
ids_C_BASIC_ITEM ci :: C_BASIC_ITEM
ci = case C_BASIC_ITEM
ci of
    CoFree_datatype al :: [Annoted CODATATYPE_DECL]
al _ ->
        ([(Set SORT, Set SORT)] -> (Set SORT, Set SORT)
unite2 ([(Set SORT, Set SORT)] -> (Set SORT, Set SORT))
-> [(Set SORT, Set SORT)] -> (Set SORT, Set SORT)
forall a b. (a -> b) -> a -> b
$ (Annoted CODATATYPE_DECL -> (Set SORT, Set SORT))
-> [Annoted CODATATYPE_DECL] -> [(Set SORT, Set SORT)]
forall a b. (a -> b) -> [a] -> [b]
map (CODATATYPE_DECL -> (Set SORT, Set SORT)
ids_CODATATYPE_DECL (CODATATYPE_DECL -> (Set SORT, Set SORT))
-> (Annoted CODATATYPE_DECL -> CODATATYPE_DECL)
-> Annoted CODATATYPE_DECL
-> (Set SORT, Set SORT)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted CODATATYPE_DECL -> CODATATYPE_DECL
forall a. Annoted a -> a
item) [Annoted CODATATYPE_DECL]
al, Set SORT
forall a. Set a
Set.empty)
    CoSort_gen al :: [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
al _ -> [IdSets] -> IdSets
unite ([IdSets] -> IdSets) -> [IdSets] -> IdSets
forall a b. (a -> b) -> a -> b
$ (Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA) -> IdSets)
-> [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)] -> [IdSets]
forall a b. (a -> b) -> [a] -> [b]
map ((C_SIG_ITEM -> IdSets) -> SIG_ITEMS C_SIG_ITEM C_FORMULA -> IdSets
forall s f. (s -> IdSets) -> SIG_ITEMS s f -> IdSets
ids_SIG_ITEMS C_SIG_ITEM -> IdSets
ids_C_SIG_ITEM (SIG_ITEMS C_SIG_ITEM C_FORMULA -> IdSets)
-> (Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)
    -> SIG_ITEMS C_SIG_ITEM C_FORMULA)
-> Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)
-> IdSets
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)
-> SIG_ITEMS C_SIG_ITEM C_FORMULA
forall a. Annoted a -> a
item) [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
al

ids_C_SIG_ITEM :: C_SIG_ITEM -> IdSets
ids_C_SIG_ITEM :: C_SIG_ITEM -> IdSets
ids_C_SIG_ITEM (CoDatatype_items al :: [Annoted CODATATYPE_DECL]
al _) =
    ([(Set SORT, Set SORT)] -> (Set SORT, Set SORT)
unite2 ([(Set SORT, Set SORT)] -> (Set SORT, Set SORT))
-> [(Set SORT, Set SORT)] -> (Set SORT, Set SORT)
forall a b. (a -> b) -> a -> b
$ (Annoted CODATATYPE_DECL -> (Set SORT, Set SORT))
-> [Annoted CODATATYPE_DECL] -> [(Set SORT, Set SORT)]
forall a b. (a -> b) -> [a] -> [b]
map (CODATATYPE_DECL -> (Set SORT, Set SORT)
ids_CODATATYPE_DECL (CODATATYPE_DECL -> (Set SORT, Set SORT))
-> (Annoted CODATATYPE_DECL -> CODATATYPE_DECL)
-> Annoted CODATATYPE_DECL
-> (Set SORT, Set SORT)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted CODATATYPE_DECL -> CODATATYPE_DECL
forall a. Annoted a -> a
item) [Annoted CODATATYPE_DECL]
al, Set SORT
forall a. Set a
Set.empty)

ids_CODATATYPE_DECL :: CODATATYPE_DECL -> (Set.Set Id, Set.Set Id)
ids_CODATATYPE_DECL :: CODATATYPE_DECL -> (Set SORT, Set SORT)
ids_CODATATYPE_DECL (CoDatatype_decl _ al :: [Annoted COALTERNATIVE]
al _) =
    [(Set SORT, Set SORT)] -> (Set SORT, Set SORT)
unite2 ([(Set SORT, Set SORT)] -> (Set SORT, Set SORT))
-> [(Set SORT, Set SORT)] -> (Set SORT, Set SORT)
forall a b. (a -> b) -> a -> b
$ (Annoted COALTERNATIVE -> (Set SORT, Set SORT))
-> [Annoted COALTERNATIVE] -> [(Set SORT, Set SORT)]
forall a b. (a -> b) -> [a] -> [b]
map (COALTERNATIVE -> (Set SORT, Set SORT)
ids_COALTERNATIVE (COALTERNATIVE -> (Set SORT, Set SORT))
-> (Annoted COALTERNATIVE -> COALTERNATIVE)
-> Annoted COALTERNATIVE
-> (Set SORT, Set SORT)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted COALTERNATIVE -> COALTERNATIVE
forall a. Annoted a -> a
item) [Annoted COALTERNATIVE]
al

ids_COALTERNATIVE :: COALTERNATIVE -> (Set.Set Id, Set.Set Id)
ids_COALTERNATIVE :: COALTERNATIVE -> (Set SORT, Set SORT)
ids_COALTERNATIVE a :: COALTERNATIVE
a = let e :: Set a
e = Set a
forall a. Set a
Set.empty in case COALTERNATIVE
a of
    Co_construct _ mi :: Maybe SORT
mi cs :: [COCOMPONENTS]
cs _ -> let s :: Set SORT
s = Set SORT -> (SORT -> Set SORT) -> Maybe SORT -> Set SORT
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set SORT
forall a. Set a
Set.empty SORT -> Set SORT
forall a. a -> Set a
Set.singleton Maybe SORT
mi in
        if [COCOMPONENTS] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [COCOMPONENTS]
cs then (Set SORT
s, Set SORT
forall a. Set a
e) else
            (Set SORT
forall a. Set a
e, [Set SORT] -> Set SORT
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set SORT] -> Set SORT) -> [Set SORT] -> Set SORT
forall a b. (a -> b) -> a -> b
$ Set SORT
s Set SORT -> [Set SORT] -> [Set SORT]
forall a. a -> [a] -> [a]
: (COCOMPONENTS -> Set SORT) -> [COCOMPONENTS] -> [Set SORT]
forall a b. (a -> b) -> [a] -> [b]
map COCOMPONENTS -> Set SORT
ids_COCOMPONENTS [COCOMPONENTS]
cs)
    CoSubsorts _ _ -> (Set SORT
forall a. Set a
e, Set SORT
forall a. Set a
e)

ids_COCOMPONENTS :: COCOMPONENTS -> Set.Set Id
ids_COCOMPONENTS :: COCOMPONENTS -> Set SORT
ids_COCOMPONENTS (CoSelect l :: [SORT]
l _ _) = [Set SORT] -> Set SORT
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set SORT] -> Set SORT) -> [Set SORT] -> Set SORT
forall a b. (a -> b) -> a -> b
$ (SORT -> Set SORT) -> [SORT] -> [Set SORT]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Set SORT
forall a. a -> Set a
Set.singleton [SORT]
l

data CoRecord a b c d = CoRecord
    { CoRecord a b c d -> C_FORMULA -> Bool -> d -> a -> Range -> c
foldBoxOrDiamond :: C_FORMULA -> Bool -> d -> a -> Range -> c
    , CoRecord a b c d -> C_FORMULA -> [SORT] -> [OP_SYMB] -> Bool -> c
foldCoSort_gen_ax :: C_FORMULA -> [SORT] -> [OP_SYMB] -> Bool -> c
    , CoRecord a b c d -> MODALITY -> b -> d
foldTerm_mod :: MODALITY -> b -> d
    , CoRecord a b c d -> MODALITY -> SIMPLE_ID -> d
foldSimple_mod :: MODALITY -> SIMPLE_ID -> d
    }

foldC_Formula :: Record C_FORMULA a b -> CoRecord a b c d -> C_FORMULA -> c
foldC_Formula :: Record C_FORMULA a b -> CoRecord a b c d -> C_FORMULA -> c
foldC_Formula r :: Record C_FORMULA a b
r cr :: CoRecord a b c d
cr c :: C_FORMULA
c = case C_FORMULA
c of
    BoxOrDiamond b :: Bool
b m :: MODALITY
m f :: FORMULA C_FORMULA
f ps :: Range
ps ->
        CoRecord a b c d -> C_FORMULA -> Bool -> d -> a -> Range -> c
forall a b c d.
CoRecord a b c d -> C_FORMULA -> Bool -> d -> a -> Range -> c
foldBoxOrDiamond CoRecord a b c d
cr C_FORMULA
c Bool
b (Record C_FORMULA a b -> CoRecord a b c d -> MODALITY -> d
forall a b c d.
Record C_FORMULA a b -> CoRecord a b c d -> MODALITY -> d
foldModality Record C_FORMULA a b
r CoRecord a b c d
cr MODALITY
m) (Record C_FORMULA a b -> FORMULA C_FORMULA -> a
forall f a b. Record f a b -> FORMULA f -> a
foldFormula Record C_FORMULA a b
r FORMULA C_FORMULA
f) Range
ps
    CoSort_gen_ax s :: [SORT]
s o :: [OP_SYMB]
o b :: Bool
b -> CoRecord a b c d -> C_FORMULA -> [SORT] -> [OP_SYMB] -> Bool -> c
forall a b c d.
CoRecord a b c d -> C_FORMULA -> [SORT] -> [OP_SYMB] -> Bool -> c
foldCoSort_gen_ax CoRecord a b c d
cr C_FORMULA
c [SORT]
s [OP_SYMB]
o Bool
b

foldModality :: Record C_FORMULA a b -> CoRecord a b c d -> MODALITY -> d
foldModality :: Record C_FORMULA a b -> CoRecord a b c d -> MODALITY -> d
foldModality r :: Record C_FORMULA a b
r cr :: CoRecord a b c d
cr m :: MODALITY
m = case MODALITY
m of
    Term_mod t :: TERM C_FORMULA
t -> CoRecord a b c d -> MODALITY -> b -> d
forall a b c d. CoRecord a b c d -> MODALITY -> b -> d
foldTerm_mod CoRecord a b c d
cr MODALITY
m (b -> d) -> b -> d
forall a b. (a -> b) -> a -> b
$ Record C_FORMULA a b -> TERM C_FORMULA -> b
forall f a b. Record f a b -> TERM f -> b
foldTerm Record C_FORMULA a b
r TERM C_FORMULA
t
    Simple_mod i :: SIMPLE_ID
i -> CoRecord a b c d -> MODALITY -> SIMPLE_ID -> d
forall a b c d. CoRecord a b c d -> MODALITY -> SIMPLE_ID -> d
foldSimple_mod CoRecord a b c d
cr MODALITY
m SIMPLE_ID
i

mapCoRecord :: CoRecord (FORMULA C_FORMULA) (TERM C_FORMULA) C_FORMULA MODALITY
mapCoRecord :: CoRecord (FORMULA C_FORMULA) (TERM C_FORMULA) C_FORMULA MODALITY
mapCoRecord = CoRecord :: forall a b c d.
(C_FORMULA -> Bool -> d -> a -> Range -> c)
-> (C_FORMULA -> [SORT] -> [OP_SYMB] -> Bool -> c)
-> (MODALITY -> b -> d)
-> (MODALITY -> SIMPLE_ID -> d)
-> CoRecord a b c d
CoRecord
    { foldBoxOrDiamond :: C_FORMULA
-> Bool -> MODALITY -> FORMULA C_FORMULA -> Range -> C_FORMULA
foldBoxOrDiamond = (Bool -> MODALITY -> FORMULA C_FORMULA -> Range -> C_FORMULA)
-> C_FORMULA
-> Bool
-> MODALITY
-> FORMULA C_FORMULA
-> Range
-> C_FORMULA
forall a b. a -> b -> a
const Bool -> MODALITY -> FORMULA C_FORMULA -> Range -> C_FORMULA
BoxOrDiamond
    , foldCoSort_gen_ax :: C_FORMULA -> [SORT] -> [OP_SYMB] -> Bool -> C_FORMULA
foldCoSort_gen_ax = ([SORT] -> [OP_SYMB] -> Bool -> C_FORMULA)
-> C_FORMULA -> [SORT] -> [OP_SYMB] -> Bool -> C_FORMULA
forall a b. a -> b -> a
const [SORT] -> [OP_SYMB] -> Bool -> C_FORMULA
CoSort_gen_ax
    , foldTerm_mod :: MODALITY -> TERM C_FORMULA -> MODALITY
foldTerm_mod = (TERM C_FORMULA -> MODALITY)
-> MODALITY -> TERM C_FORMULA -> MODALITY
forall a b. a -> b -> a
const TERM C_FORMULA -> MODALITY
Term_mod
    , foldSimple_mod :: MODALITY -> SIMPLE_ID -> MODALITY
foldSimple_mod = (SIMPLE_ID -> MODALITY) -> MODALITY -> SIMPLE_ID -> MODALITY
forall a b. a -> b -> a
const SIMPLE_ID -> MODALITY
Simple_mod
    }

constCoRecord :: ([a] -> a) -> a -> CoRecord a a a a
constCoRecord :: ([a] -> a) -> a -> CoRecord a a a a
constCoRecord jn :: [a] -> a
jn c :: a
c = CoRecord :: forall a b c d.
(C_FORMULA -> Bool -> d -> a -> Range -> c)
-> (C_FORMULA -> [SORT] -> [OP_SYMB] -> Bool -> c)
-> (MODALITY -> b -> d)
-> (MODALITY -> SIMPLE_ID -> d)
-> CoRecord a b c d
CoRecord
    { foldBoxOrDiamond :: C_FORMULA -> Bool -> a -> a -> Range -> a
foldBoxOrDiamond = \ _ _ m :: a
m f :: a
f _ -> [a] -> a
jn [a
m, a
f]
    , foldCoSort_gen_ax :: C_FORMULA -> [SORT] -> [OP_SYMB] -> Bool -> a
foldCoSort_gen_ax = \ _ _ _ _ -> a
c
    , foldTerm_mod :: MODALITY -> a -> a
foldTerm_mod = \ _ t :: a
t -> a
t
    , foldSimple_mod :: MODALITY -> SIMPLE_ID -> a
foldSimple_mod = \ _ _ -> a
c
    }

mapC_FORMULA :: C_FORMULA -> C_FORMULA
mapC_FORMULA :: C_FORMULA -> C_FORMULA
mapC_FORMULA = Record C_FORMULA (FORMULA C_FORMULA) (TERM C_FORMULA)
-> CoRecord (FORMULA C_FORMULA) (TERM C_FORMULA) C_FORMULA MODALITY
-> C_FORMULA
-> C_FORMULA
forall a b c d.
Record C_FORMULA a b -> CoRecord a b c d -> C_FORMULA -> c
foldC_Formula ((C_FORMULA -> C_FORMULA)
-> Record C_FORMULA (FORMULA C_FORMULA) (TERM C_FORMULA)
forall f. (f -> f) -> Record f (FORMULA f) (TERM f)
mkMixfixRecord C_FORMULA -> C_FORMULA
mapC_FORMULA) CoRecord (FORMULA C_FORMULA) (TERM C_FORMULA) C_FORMULA MODALITY
mapCoRecord

resolveMODALITY :: MixResolve MODALITY
resolveMODALITY :: MixResolve MODALITY
resolveMODALITY ga :: GlobalAnnos
ga ids :: (TokRules, Rules)
ids m :: MODALITY
m = case MODALITY
m of
    Term_mod t :: TERM C_FORMULA
t ->
        (TERM C_FORMULA -> MODALITY)
-> Result (TERM C_FORMULA) -> Result MODALITY
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TERM C_FORMULA -> MODALITY
Term_mod (Result (TERM C_FORMULA) -> Result MODALITY)
-> Result (TERM C_FORMULA) -> Result MODALITY
forall a b. (a -> b) -> a -> b
$ (C_FORMULA -> C_FORMULA)
-> MixResolve C_FORMULA -> MixResolve (TERM C_FORMULA)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (TERM f)
resolveMixTrm C_FORMULA -> C_FORMULA
mapC_FORMULA MixResolve C_FORMULA
resolveC_FORMULA GlobalAnnos
ga (TokRules, Rules)
ids TERM C_FORMULA
t
    _ -> MODALITY -> Result MODALITY
forall (m :: * -> *) a. Monad m => a -> m a
return MODALITY
m

resolveC_FORMULA :: MixResolve C_FORMULA
resolveC_FORMULA :: MixResolve C_FORMULA
resolveC_FORMULA ga :: GlobalAnnos
ga ids :: (TokRules, Rules)
ids cf :: C_FORMULA
cf = case C_FORMULA
cf of
   BoxOrDiamond b :: Bool
b m :: MODALITY
m f :: FORMULA C_FORMULA
f ps :: Range
ps -> do
       MODALITY
nm <- MixResolve MODALITY
resolveMODALITY GlobalAnnos
ga (TokRules, Rules)
ids MODALITY
m
       FORMULA C_FORMULA
nf <- (C_FORMULA -> C_FORMULA)
-> MixResolve C_FORMULA -> MixResolve (FORMULA C_FORMULA)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveMixFrm C_FORMULA -> C_FORMULA
mapC_FORMULA MixResolve C_FORMULA
resolveC_FORMULA GlobalAnnos
ga (TokRules, Rules)
ids FORMULA C_FORMULA
f
       C_FORMULA -> Result C_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (C_FORMULA -> Result C_FORMULA) -> C_FORMULA -> Result C_FORMULA
forall a b. (a -> b) -> a -> b
$ Bool -> MODALITY -> FORMULA C_FORMULA -> Range -> C_FORMULA
BoxOrDiamond Bool
b MODALITY
nm FORMULA C_FORMULA
nf Range
ps
   _ -> [Char] -> Result C_FORMULA
forall a. HasCallStack => [Char] -> a
error "resolveC_FORMULA"

minExpForm :: Min C_FORMULA CoCASLSign
minExpForm :: Min C_FORMULA CoCASLSign
minExpForm s :: Sign C_FORMULA CoCASLSign
s form :: C_FORMULA
form =
    let ops :: Set SORT
ops = Sign C_FORMULA CoCASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
formulaIds Sign C_FORMULA CoCASLSign
s
        minMod :: MODALITY -> t -> Result MODALITY
minMod md :: MODALITY
md ps :: t
ps = case MODALITY
md of
                  Simple_mod i :: SIMPLE_ID
i -> MODALITY -> t -> Result MODALITY
minMod (TERM C_FORMULA -> MODALITY
Term_mod (SIMPLE_ID -> TERM C_FORMULA
forall f. SIMPLE_ID -> TERM f
Mixfix_token SIMPLE_ID
i)) t
ps
                  Term_mod t :: TERM C_FORMULA
t -> let
                    r :: Result MODALITY
r = do
                      TERM C_FORMULA
t2 <- Min C_FORMULA CoCASLSign
-> Sign C_FORMULA CoCASLSign
-> TERM C_FORMULA
-> Result (TERM C_FORMULA)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result (TERM f)
oneExpTerm Min C_FORMULA CoCASLSign
minExpForm Sign C_FORMULA CoCASLSign
s TERM C_FORMULA
t
                      let srt :: SORT
srt = TERM C_FORMULA -> SORT
forall f. TermExtension f => f -> SORT
sortOfTerm TERM C_FORMULA
t2
                          trm :: MODALITY
trm = TERM C_FORMULA -> MODALITY
Term_mod TERM C_FORMULA
t2
                      if SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
srt Set SORT
ops
                         then MODALITY -> Result MODALITY
forall (m :: * -> *) a. Monad m => a -> m a
return MODALITY
trm
                         else [Diagnosis] -> Maybe MODALITY -> Result MODALITY
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> [Char] -> TERM C_FORMULA -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error
                              ("unknown modality '"
                               [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SORT -> [Char] -> [Char]
showId SORT
srt "' for term") TERM C_FORMULA
t ]
                              (Maybe MODALITY -> Result MODALITY)
-> Maybe MODALITY -> Result MODALITY
forall a b. (a -> b) -> a -> b
$ MODALITY -> Maybe MODALITY
forall a. a -> Maybe a
Just MODALITY
trm
                    in case TERM C_FORMULA
t of
                       Mixfix_token tm :: SIMPLE_ID
tm ->
                           if SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (SIMPLE_ID -> SORT
simpleIdToId SIMPLE_ID
tm) Set SORT
ops
                              then MODALITY -> Result MODALITY
forall (m :: * -> *) a. Monad m => a -> m a
return (MODALITY -> Result MODALITY) -> MODALITY -> Result MODALITY
forall a b. (a -> b) -> a -> b
$ SIMPLE_ID -> MODALITY
Simple_mod SIMPLE_ID
tm
                              else case Result MODALITY -> Maybe MODALITY
forall a. Result a -> Maybe a
maybeResult Result MODALITY
r of
                                  Nothing -> [Diagnosis] -> Maybe MODALITY -> Result MODALITY
forall a. [Diagnosis] -> Maybe a -> Result a
Result
                                      [DiagKind -> [Char] -> SIMPLE_ID -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error "unknown modality" SIMPLE_ID
tm]
                                      (Maybe MODALITY -> Result MODALITY)
-> Maybe MODALITY -> Result MODALITY
forall a b. (a -> b) -> a -> b
$ MODALITY -> Maybe MODALITY
forall a. a -> Maybe a
Just (MODALITY -> Maybe MODALITY) -> MODALITY -> Maybe MODALITY
forall a b. (a -> b) -> a -> b
$ SIMPLE_ID -> MODALITY
Simple_mod SIMPLE_ID
tm
                                  _ -> Result MODALITY
r
                       _ -> Result MODALITY
r
    in case C_FORMULA
form of
        BoxOrDiamond b :: Bool
b m :: MODALITY
m f :: FORMULA C_FORMULA
f ps :: Range
ps ->
            do MODALITY
nm <- MODALITY -> Range -> Result MODALITY
forall t. MODALITY -> t -> Result MODALITY
minMod MODALITY
m Range
ps
               FORMULA C_FORMULA
f2 <- Min C_FORMULA CoCASLSign
-> Sign C_FORMULA CoCASLSign
-> FORMULA C_FORMULA
-> Result (FORMULA C_FORMULA)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min C_FORMULA CoCASLSign
minExpForm Sign C_FORMULA CoCASLSign
s FORMULA C_FORMULA
f
               C_FORMULA -> Result C_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (C_FORMULA -> Result C_FORMULA) -> C_FORMULA -> Result C_FORMULA
forall a b. (a -> b) -> a -> b
$ Bool -> MODALITY -> FORMULA C_FORMULA -> Range -> C_FORMULA
BoxOrDiamond Bool
b MODALITY
nm FORMULA C_FORMULA
f2 Range
ps
        phi :: C_FORMULA
phi -> C_FORMULA -> Result C_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return C_FORMULA
phi

ana_C_SIG_ITEM :: Ana C_SIG_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
ana_C_SIG_ITEM :: Ana C_SIG_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
ana_C_SIG_ITEM _ mi :: C_SIG_ITEM
mi = case C_SIG_ITEM
mi of
    CoDatatype_items al :: [Annoted CODATATYPE_DECL]
al _ ->
        do (Annoted CODATATYPE_DECL -> State (Sign C_FORMULA CoCASLSign) ())
-> [Annoted CODATATYPE_DECL]
-> State (Sign C_FORMULA CoCASLSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ i :: Annoted CODATATYPE_DECL
i -> case Annoted CODATATYPE_DECL -> CODATATYPE_DECL
forall a. Annoted a -> a
item Annoted CODATATYPE_DECL
i of
                  CoDatatype_decl s :: SORT
s _ _ -> SortsKind
-> Annoted CODATATYPE_DECL
-> SORT
-> State (Sign C_FORMULA CoCASLSign) ()
forall a f e. SortsKind -> Annoted a -> SORT -> State (Sign f e) ()
addSort SortsKind
NonEmptySorts Annoted CODATATYPE_DECL
i SORT
s) [Annoted CODATATYPE_DECL]
al
           (CODATATYPE_DECL -> State (Sign C_FORMULA CoCASLSign) [Component])
-> [Annoted CODATATYPE_DECL]
-> State (Sign C_FORMULA CoCASLSign) [Annoted [Component]]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM (GenKind
-> CODATATYPE_DECL -> State (Sign C_FORMULA CoCASLSign) [Component]
ana_CODATATYPE_DECL GenKind
Loose) [Annoted CODATATYPE_DECL]
al
           State (Sign C_FORMULA CoCASLSign) ()
forall f e. State (Sign f e) ()
closeSubsortRel
           C_SIG_ITEM -> State (Sign C_FORMULA CoCASLSign) C_SIG_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return C_SIG_ITEM
mi

isCoConsAlt :: COALTERNATIVE -> Bool
isCoConsAlt :: COALTERNATIVE -> Bool
isCoConsAlt a :: COALTERNATIVE
a = case COALTERNATIVE
a of
                CoSubsorts _ _ -> Bool
False
                _ -> Bool
True

getCoSubsorts :: COALTERNATIVE -> [SORT]
getCoSubsorts :: COALTERNATIVE -> [SORT]
getCoSubsorts c :: COALTERNATIVE
c = case COALTERNATIVE
c of
    CoSubsorts cs :: [SORT]
cs _ -> [SORT]
cs
    _ -> []

-- | return list of constructors
ana_CODATATYPE_DECL :: GenKind -> CODATATYPE_DECL -> State CSign [Component]
ana_CODATATYPE_DECL :: GenKind
-> CODATATYPE_DECL -> State (Sign C_FORMULA CoCASLSign) [Component]
ana_CODATATYPE_DECL gk :: GenKind
gk (CoDatatype_decl s :: SORT
s al :: [Annoted COALTERNATIVE]
al _) = do
       [Maybe (Component, Set Component)]
ul <- (Annoted COALTERNATIVE
 -> State
      (Sign C_FORMULA CoCASLSign) (Maybe (Component, Set Component)))
-> [Annoted COALTERNATIVE]
-> State
     (Sign C_FORMULA CoCASLSign) [Maybe (Component, Set Component)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SORT
-> Annoted COALTERNATIVE
-> State
     (Sign C_FORMULA CoCASLSign) (Maybe (Component, Set Component))
ana_COALTERNATIVE SORT
s) [Annoted COALTERNATIVE]
al
       let constr :: [(Component, Set Component)]
constr = [Maybe (Component, Set Component)] -> [(Component, Set Component)]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (Component, Set Component)]
ul
           cs :: [Component]
cs = ((Component, Set Component) -> Component)
-> [(Component, Set Component)] -> [Component]
forall a b. (a -> b) -> [a] -> [b]
map (Component, Set Component) -> Component
forall a b. (a, b) -> a
fst [(Component, Set Component)]
constr
       Bool
-> State (Sign C_FORMULA CoCASLSign) ()
-> State (Sign C_FORMULA CoCASLSign) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(Component, Set Component)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Component, Set Component)]
constr) (State (Sign C_FORMULA CoCASLSign) ()
 -> State (Sign C_FORMULA CoCASLSign) ())
-> State (Sign C_FORMULA CoCASLSign) ()
-> State (Sign C_FORMULA CoCASLSign) ()
forall a b. (a -> b) -> a -> b
$ do
                  [Diagnosis] -> State (Sign C_FORMULA CoCASLSign) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State (Sign C_FORMULA CoCASLSign) ())
-> [Diagnosis] -> State (Sign C_FORMULA CoCASLSign) ()
forall a b. (a -> b) -> a -> b
$ [Component] -> [Diagnosis]
forall a. (Pretty a, GetRange a, Ord a) => [a] -> [Diagnosis]
checkUniqueness [Component]
cs
                  let totalSels :: Set Component
totalSels = [Set Component] -> Set Component
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Component] -> Set Component)
-> [Set Component] -> Set Component
forall a b. (a -> b) -> a -> b
$ ((Component, Set Component) -> Set Component)
-> [(Component, Set Component)] -> [Set Component]
forall a b. (a -> b) -> [a] -> [b]
map (Component, Set Component) -> Set Component
forall a b. (a, b) -> b
snd [(Component, Set Component)]
constr
                      wrongConstr :: [(Component, Set Component)]
wrongConstr = ((Component, Set Component) -> Bool)
-> [(Component, Set Component)] -> [(Component, Set Component)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Set Component
totalSels Set Component -> Set Component -> Bool
forall a. Eq a => a -> a -> Bool
/=) (Set Component -> Bool)
-> ((Component, Set Component) -> Set Component)
-> (Component, Set Component)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Component, Set Component) -> Set Component
forall a b. (a, b) -> b
snd) [(Component, Set Component)]
constr
                  [Diagnosis] -> State (Sign C_FORMULA CoCASLSign) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State (Sign C_FORMULA CoCASLSign) ())
-> [Diagnosis] -> State (Sign C_FORMULA CoCASLSign) ()
forall a b. (a -> b) -> a -> b
$ ((Component, Set Component) -> Diagnosis)
-> [(Component, Set Component)] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (\ (c :: Component
c, _) -> DiagKind -> [Char] -> Component -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error
                      ("total selectors '" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ([Char] -> [Char])
-> (Component -> [Char] -> [Char])
-> [Component]
-> [Char]
-> [Char]
forall a.
([Char] -> [Char])
-> (a -> [Char] -> [Char]) -> [a] -> [Char] -> [Char]
showSepList ([Char] -> [Char] -> [Char]
showString ",")
                       Component -> [Char] -> [Char]
forall a. Pretty a => a -> [Char] -> [Char]
showDoc (Set Component -> [Component]
forall a. Set a -> [a]
Set.toList Set Component
totalSels)
                       "'\n  must appear in alternative") Component
c) [(Component, Set Component)]
wrongConstr
       case GenKind
gk of
         Free -> do
           let (alts :: [COALTERNATIVE]
alts, subs :: [COALTERNATIVE]
subs) = (COALTERNATIVE -> Bool)
-> [COALTERNATIVE] -> ([COALTERNATIVE], [COALTERNATIVE])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition COALTERNATIVE -> Bool
isCoConsAlt ([COALTERNATIVE] -> ([COALTERNATIVE], [COALTERNATIVE]))
-> [COALTERNATIVE] -> ([COALTERNATIVE], [COALTERNATIVE])
forall a b. (a -> b) -> a -> b
$ (Annoted COALTERNATIVE -> COALTERNATIVE)
-> [Annoted COALTERNATIVE] -> [COALTERNATIVE]
forall a b. (a -> b) -> [a] -> [b]
map Annoted COALTERNATIVE -> COALTERNATIVE
forall a. Annoted a -> a
item [Annoted COALTERNATIVE]
al
               sbs :: [SORT]
sbs = (COALTERNATIVE -> [SORT]) -> [COALTERNATIVE] -> [SORT]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap COALTERNATIVE -> [SORT]
getCoSubsorts [COALTERNATIVE]
subs
               comps :: [(Maybe SORT, OpType, [COCOMPONENTS])]
comps = (COALTERNATIVE -> (Maybe SORT, OpType, [COCOMPONENTS]))
-> [COALTERNATIVE] -> [(Maybe SORT, OpType, [COCOMPONENTS])]
forall a b. (a -> b) -> [a] -> [b]
map (SORT -> COALTERNATIVE -> (Maybe SORT, OpType, [COCOMPONENTS])
getCoConsType SORT
s) [COALTERNATIVE]
alts
               ttrips :: [(Maybe (SORT, TERM f), [VAR_DECL], [(SORT, OpType)])]
ttrips = ((Maybe SORT, OpType, [COCOMPONENTS])
 -> (Maybe (SORT, TERM f), [VAR_DECL], [(SORT, OpType)]))
-> [(Maybe SORT, OpType, [COCOMPONENTS])]
-> [(Maybe (SORT, TERM f), [VAR_DECL], [(SORT, OpType)])]
forall a b. (a -> b) -> [a] -> [b]
map ((\ (a :: Maybe (SORT, TERM f)
a, vs :: [VAR_DECL]
vs, ses :: [(Maybe SORT, OpType)]
ses) -> (Maybe (SORT, TERM f)
a, [VAR_DECL]
vs, [(Maybe SORT, OpType)] -> [(SORT, OpType)]
catSels [(Maybe SORT, OpType)]
ses))
                            ((Maybe (SORT, TERM f), [VAR_DECL], [(Maybe SORT, OpType)])
 -> (Maybe (SORT, TERM f), [VAR_DECL], [(SORT, OpType)]))
-> ((Maybe SORT, OpType, [COCOMPONENTS])
    -> (Maybe (SORT, TERM f), [VAR_DECL], [(Maybe SORT, OpType)]))
-> (Maybe SORT, OpType, [COCOMPONENTS])
-> (Maybe (SORT, TERM f), [VAR_DECL], [(SORT, OpType)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char]
-> (Maybe SORT, OpType, [COCOMPONENTS])
-> (Maybe (SORT, TERM f), [VAR_DECL], [(Maybe SORT, OpType)])
forall f.
[Char]
-> (Maybe SORT, OpType, [COCOMPONENTS])
-> (Maybe (SORT, TERM f), [VAR_DECL], [(Maybe SORT, OpType)])
coselForms1 "X") [(Maybe SORT, OpType, [COCOMPONENTS])]
comps
               sels :: [(SORT, OpType)]
sels = ((Maybe (SORT, TERM Any), [VAR_DECL], [(SORT, OpType)])
 -> [(SORT, OpType)])
-> [(Maybe (SORT, TERM Any), [VAR_DECL], [(SORT, OpType)])]
-> [(SORT, OpType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (_, _, ses :: [(SORT, OpType)]
ses) -> [(SORT, OpType)]
ses) [(Maybe (SORT, TERM Any), [VAR_DECL], [(SORT, OpType)])]
forall f. [(Maybe (SORT, TERM f), [VAR_DECL], [(SORT, OpType)])]
ttrips
           [Named (FORMULA C_FORMULA)] -> State (Sign C_FORMULA CoCASLSign) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences ([Named (FORMULA C_FORMULA)]
 -> State (Sign C_FORMULA CoCASLSign) ())
-> [Named (FORMULA C_FORMULA)]
-> State (Sign C_FORMULA CoCASLSign) ()
forall a b. (a -> b) -> a -> b
$ ((Maybe SORT, OpType, [COCOMPONENTS])
 -> Maybe (Named (FORMULA C_FORMULA)))
-> [(Maybe SORT, OpType, [COCOMPONENTS])]
-> [Named (FORMULA C_FORMULA)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Maybe SORT, OpType, [COCOMPONENTS])
-> Maybe (Named (FORMULA C_FORMULA))
forall f.
(Maybe SORT, OpType, [COCOMPONENTS]) -> Maybe (Named (FORMULA f))
comakeInjective
                            ([(Maybe SORT, OpType, [COCOMPONENTS])]
 -> [Named (FORMULA C_FORMULA)])
-> [(Maybe SORT, OpType, [COCOMPONENTS])]
-> [Named (FORMULA C_FORMULA)]
forall a b. (a -> b) -> a -> b
$ ((Maybe SORT, OpType, [COCOMPONENTS]) -> Bool)
-> [(Maybe SORT, OpType, [COCOMPONENTS])]
-> [(Maybe SORT, OpType, [COCOMPONENTS])]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, _, ces :: [COCOMPONENTS]
ces) -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [COCOMPONENTS] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [COCOMPONENTS]
ces)
                              [(Maybe SORT, OpType, [COCOMPONENTS])]
comps
           [Named (FORMULA C_FORMULA)] -> State (Sign C_FORMULA CoCASLSign) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences ([Named (FORMULA C_FORMULA)]
 -> State (Sign C_FORMULA CoCASLSign) ())
-> [Named (FORMULA C_FORMULA)]
-> State (Sign C_FORMULA CoCASLSign) ()
forall a b. (a -> b) -> a -> b
$ SORT -> [SORT] -> [Named (FORMULA C_FORMULA)]
forall f. SORT -> [SORT] -> [Named (FORMULA f)]
makeDisjSubsorts SORT
s [SORT]
sbs
           [Named (FORMULA C_FORMULA)] -> State (Sign C_FORMULA CoCASLSign) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences ([Named (FORMULA C_FORMULA)]
 -> State (Sign C_FORMULA CoCASLSign) ())
-> [Named (FORMULA C_FORMULA)]
-> State (Sign C_FORMULA CoCASLSign) ()
forall a b. (a -> b) -> a -> b
$ [Maybe (Named (FORMULA C_FORMULA))] -> [Named (FORMULA C_FORMULA)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Named (FORMULA C_FORMULA))]
 -> [Named (FORMULA C_FORMULA)])
-> [Maybe (Named (FORMULA C_FORMULA))]
-> [Named (FORMULA C_FORMULA)]
forall a b. (a -> b) -> a -> b
$ ((Maybe SORT, OpType, [COCOMPONENTS])
 -> [Maybe (Named (FORMULA C_FORMULA))])
-> [(Maybe SORT, OpType, [COCOMPONENTS])]
-> [Maybe (Named (FORMULA C_FORMULA))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
                            (\ c :: (Maybe SORT, OpType, [COCOMPONENTS])
c -> (SORT -> Maybe (Named (FORMULA C_FORMULA)))
-> [SORT] -> [Maybe (Named (FORMULA C_FORMULA))]
forall a b. (a -> b) -> [a] -> [b]
map ((Maybe SORT, OpType, [COCOMPONENTS])
-> SORT -> Maybe (Named (FORMULA C_FORMULA))
forall f.
(Maybe SORT, OpType, [COCOMPONENTS])
-> SORT -> Maybe (Named (FORMULA f))
comakeDisjToSort (Maybe SORT, OpType, [COCOMPONENTS])
c) [SORT]
sbs)
                        [(Maybe SORT, OpType, [COCOMPONENTS])]
comps
           [Named (FORMULA C_FORMULA)] -> State (Sign C_FORMULA CoCASLSign) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences ([Named (FORMULA C_FORMULA)]
 -> State (Sign C_FORMULA CoCASLSign) ())
-> [Named (FORMULA C_FORMULA)]
-> State (Sign C_FORMULA CoCASLSign) ()
forall a b. (a -> b) -> a -> b
$ [(Maybe SORT, OpType, [COCOMPONENTS])]
-> [Named (FORMULA C_FORMULA)]
forall f.
[(Maybe SORT, OpType, [COCOMPONENTS])] -> [Named (FORMULA f)]
comakeDisjoint [(Maybe SORT, OpType, [COCOMPONENTS])]
comps
           let ttrips' :: [(SORT, [VAR_DECL], TERM f, [(SORT, OpType)])]
ttrips' = [(SORT
a, [VAR_DECL]
vs, TERM f
t, [(SORT, OpType)]
ses) | (Just (a :: SORT
a, t :: TERM f
t), vs :: [VAR_DECL]
vs, ses :: [(SORT, OpType)]
ses) <- [(Maybe (SORT, TERM f), [VAR_DECL], [(SORT, OpType)])]
forall f. [(Maybe (SORT, TERM f), [VAR_DECL], [(SORT, OpType)])]
ttrips]
           [Named (FORMULA C_FORMULA)] -> State (Sign C_FORMULA CoCASLSign) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences ([Named (FORMULA C_FORMULA)]
 -> State (Sign C_FORMULA CoCASLSign) ())
-> [Named (FORMULA C_FORMULA)]
-> State (Sign C_FORMULA CoCASLSign) ()
forall a b. (a -> b) -> a -> b
$ [Maybe (Named (FORMULA C_FORMULA))] -> [Named (FORMULA C_FORMULA)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Named (FORMULA C_FORMULA))]
 -> [Named (FORMULA C_FORMULA)])
-> [Maybe (Named (FORMULA C_FORMULA))]
-> [Named (FORMULA C_FORMULA)]
forall a b. (a -> b) -> a -> b
$ ((SORT, OpType) -> [Maybe (Named (FORMULA C_FORMULA))])
-> [(SORT, OpType)] -> [Maybe (Named (FORMULA C_FORMULA))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
                             (\ ses :: (SORT, OpType)
ses ->
                               ((SORT, [VAR_DECL], TERM C_FORMULA, [(SORT, OpType)])
 -> Maybe (Named (FORMULA C_FORMULA)))
-> [(SORT, [VAR_DECL], TERM C_FORMULA, [(SORT, OpType)])]
-> [Maybe (Named (FORMULA C_FORMULA))]
forall a b. (a -> b) -> [a] -> [b]
map ((SORT, OpType)
-> (SORT, [VAR_DECL], TERM C_FORMULA, [(SORT, OpType)])
-> Maybe (Named (FORMULA C_FORMULA))
forall f.
(SORT, OpType)
-> (SORT, [VAR_DECL], TERM f, [(SORT, OpType)])
-> Maybe (Named (FORMULA f))
makeUndefForm (SORT, OpType)
ses) [(SORT, [VAR_DECL], TERM C_FORMULA, [(SORT, OpType)])]
forall f. [(SORT, [VAR_DECL], TERM f, [(SORT, OpType)])]
ttrips') [(SORT, OpType)]
sels
         _ -> () -> State (Sign C_FORMULA CoCASLSign) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       [Component] -> State (Sign C_FORMULA CoCASLSign) [Component]
forall (m :: * -> *) a. Monad m => a -> m a
return [Component]
cs

getCoConsType :: SORT -> COALTERNATIVE -> (Maybe Id, OpType, [COCOMPONENTS])
getCoConsType :: SORT -> COALTERNATIVE -> (Maybe SORT, OpType, [COCOMPONENTS])
getCoConsType s :: SORT
s c :: COALTERNATIVE
c =
    let (part :: OpKind
part, i :: Maybe SORT
i, il :: [COCOMPONENTS]
il) = case COALTERNATIVE
c of
              CoSubsorts _ _ -> [Char] -> (OpKind, Maybe SORT, [COCOMPONENTS])
forall a. HasCallStack => [Char] -> a
error "getCoConsType"
              Co_construct k :: OpKind
k a :: Maybe SORT
a l :: [COCOMPONENTS]
l _ -> (OpKind
k, Maybe SORT
a, [COCOMPONENTS]
l)
        in (Maybe SORT
i, OpKind -> [SORT] -> SORT -> OpType
OpType OpKind
part ((COCOMPONENTS -> [SORT]) -> [COCOMPONENTS] -> [SORT]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
                            (((SORT, OpType) -> SORT) -> [(SORT, OpType)] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (OpType -> SORT
opRes (OpType -> SORT)
-> ((SORT, OpType) -> OpType) -> (SORT, OpType) -> SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SORT, OpType) -> OpType
forall a b. (a, b) -> b
snd) ([(SORT, OpType)] -> [SORT])
-> (COCOMPONENTS -> [(SORT, OpType)]) -> COCOMPONENTS -> [SORT]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> COCOMPONENTS -> [(SORT, OpType)]
getCoCompType SORT
s) [COCOMPONENTS]
il) SORT
s, [COCOMPONENTS]
il)

getCoCompType :: SORT -> COCOMPONENTS -> [(Id, OpType)]
getCoCompType :: SORT -> COCOMPONENTS -> [(SORT, OpType)]
getCoCompType s :: SORT
s (CoSelect l :: [SORT]
l (Op_type k :: OpKind
k args :: [SORT]
args res :: SORT
res _) _) =
    (SORT -> (SORT, OpType)) -> [SORT] -> [(SORT, OpType)]
forall a b. (a -> b) -> [a] -> [b]
map (\ i :: SORT
i -> (SORT
i, OpKind -> [SORT] -> SORT -> OpType
OpType OpKind
k ([SORT]
args [SORT] -> [SORT] -> [SORT]
forall a. [a] -> [a] -> [a]
++ [SORT
s]) SORT
res)) [SORT]
l

coselForms :: (Maybe Id, OpType, [COCOMPONENTS]) -> [Named (FORMULA f)]
coselForms :: (Maybe SORT, OpType, [COCOMPONENTS]) -> [Named (FORMULA f)]
coselForms x :: (Maybe SORT, OpType, [COCOMPONENTS])
x = case [Char]
-> (Maybe SORT, OpType, [COCOMPONENTS])
-> (Maybe (SORT, TERM f), [VAR_DECL], [(Maybe SORT, OpType)])
forall f.
[Char]
-> (Maybe SORT, OpType, [COCOMPONENTS])
-> (Maybe (SORT, TERM f), [VAR_DECL], [(Maybe SORT, OpType)])
coselForms1 "X" (Maybe SORT, OpType, [COCOMPONENTS])
x of
    (Just (i :: SORT
i, f :: TERM f
f), vs :: [VAR_DECL]
vs, cs :: [(Maybe SORT, OpType)]
cs) -> Int
-> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
-> [Named (FORMULA f)]
forall f.
Int
-> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
-> [Named (FORMULA f)]
makeSelForms 1 (SORT
i, [VAR_DECL]
vs, TERM f
f, [(Maybe SORT, OpType)]
cs)
    _ -> []

coselForms1 :: String -> (Maybe Id, OpType, [COCOMPONENTS])
          -> (Maybe (Id, TERM f), [VAR_DECL], [(Maybe Id, OpType)])
coselForms1 :: [Char]
-> (Maybe SORT, OpType, [COCOMPONENTS])
-> (Maybe (SORT, TERM f), [VAR_DECL], [(Maybe SORT, OpType)])
coselForms1 str :: [Char]
str (i :: Maybe SORT
i, ty :: OpType
ty, il :: [COCOMPONENTS]
il) =
    let cs :: [(SORT, OpType)]
cs = (COCOMPONENTS -> [(SORT, OpType)])
-> [COCOMPONENTS] -> [(SORT, OpType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SORT -> COCOMPONENTS -> [(SORT, OpType)]
getCoCompType (SORT -> COCOMPONENTS -> [(SORT, OpType)])
-> SORT -> COCOMPONENTS -> [(SORT, OpType)]
forall a b. (a -> b) -> a -> b
$ OpType -> SORT
opRes OpType
ty) [COCOMPONENTS]
il
        vs :: [VAR_DECL]
vs = [Char] -> Int -> [OpType] -> [VAR_DECL]
genSelVars [Char]
str 1 ([OpType] -> [VAR_DECL]) -> [OpType] -> [VAR_DECL]
forall a b. (a -> b) -> a -> b
$ ((SORT, OpType) -> OpType) -> [(SORT, OpType)] -> [OpType]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, OpType) -> OpType
forall a b. (a, b) -> b
snd [(SORT, OpType)]
cs
        it :: Maybe (SORT, TERM f)
it = case Maybe SORT
i of
               Nothing -> Maybe (SORT, TERM f)
forall a. Maybe a
Nothing
               Just i' :: SORT
i' -> (SORT, TERM f) -> Maybe (SORT, TERM f)
forall a. a -> Maybe a
Just (SORT
i', OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
i'
                                                 (OpType -> OP_TYPE
toOP_TYPE OpType
ty) Range
nullRange)
                                              ((VAR_DECL -> TERM f) -> [VAR_DECL] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar [VAR_DECL]
vs) Range
nullRange)
     in (Maybe (SORT, TERM f)
forall f. Maybe (SORT, TERM f)
it, [VAR_DECL]
vs, ((SORT, OpType) -> (Maybe SORT, OpType))
-> [(SORT, OpType)] -> [(Maybe SORT, OpType)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (j :: SORT
j, typ :: OpType
typ) -> (SORT -> Maybe SORT
forall a. a -> Maybe a
Just SORT
j, OpType
typ)) [(SORT, OpType)]
cs)

comakeDisjToSort :: (Maybe Id, OpType, [COCOMPONENTS]) -> SORT
                     -> Maybe (Named (FORMULA f))
comakeDisjToSort :: (Maybe SORT, OpType, [COCOMPONENTS])
-> SORT -> Maybe (Named (FORMULA f))
comakeDisjToSort a :: (Maybe SORT, OpType, [COCOMPONENTS])
a s :: SORT
s = do
    let (i :: Maybe (SORT, TERM f)
i, v :: [VAR_DECL]
v, _) = [Char]
-> (Maybe SORT, OpType, [COCOMPONENTS])
-> (Maybe (SORT, TERM f), [VAR_DECL], [(Maybe SORT, OpType)])
forall f.
[Char]
-> (Maybe SORT, OpType, [COCOMPONENTS])
-> (Maybe (SORT, TERM f), [VAR_DECL], [(Maybe SORT, OpType)])
coselForms1 "X" (Maybe SORT, OpType, [COCOMPONENTS])
a
        p :: Range
p = SORT -> Range
posOfId SORT
s
    (c :: SORT
c, t :: TERM f
t) <- Maybe (SORT, TERM f)
forall f. Maybe (SORT, TERM f)
i
    Named (FORMULA f) -> Maybe (Named (FORMULA f))
forall (m :: * -> *) a. Monad m => a -> m a
return (Named (FORMULA f) -> Maybe (Named (FORMULA f)))
-> Named (FORMULA f) -> Maybe (Named (FORMULA f))
forall a b. (a -> b) -> a -> b
$ [Char] -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_disjoint_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SORT -> [Char] -> [Char]
showId SORT
c "_sort_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SORT -> [Char] -> [Char]
showId SORT
s "")
               (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange [VAR_DECL]
v (FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Range -> FORMULA f
Negation (TERM f -> SORT -> Range -> FORMULA f
forall f. TERM f -> SORT -> Range -> FORMULA f
Membership TERM f
t SORT
s Range
p) Range
p) Range
p

comakeInjective :: (Maybe Id, OpType, [COCOMPONENTS])
                     -> Maybe (Named (FORMULA f))
comakeInjective :: (Maybe SORT, OpType, [COCOMPONENTS]) -> Maybe (Named (FORMULA f))
comakeInjective a :: (Maybe SORT, OpType, [COCOMPONENTS])
a = do
    let (i1 :: Maybe (SORT, TERM f)
i1, v1 :: [VAR_DECL]
v1, _) = [Char]
-> (Maybe SORT, OpType, [COCOMPONENTS])
-> (Maybe (SORT, TERM f), [VAR_DECL], [(Maybe SORT, OpType)])
forall f.
[Char]
-> (Maybe SORT, OpType, [COCOMPONENTS])
-> (Maybe (SORT, TERM f), [VAR_DECL], [(Maybe SORT, OpType)])
coselForms1 "X" (Maybe SORT, OpType, [COCOMPONENTS])
a
        (i2 :: Maybe (SORT, TERM f)
i2, v2 :: [VAR_DECL]
v2, _) = [Char]
-> (Maybe SORT, OpType, [COCOMPONENTS])
-> (Maybe (SORT, TERM f), [VAR_DECL], [(Maybe SORT, OpType)])
forall f.
[Char]
-> (Maybe SORT, OpType, [COCOMPONENTS])
-> (Maybe (SORT, TERM f), [VAR_DECL], [(Maybe SORT, OpType)])
coselForms1 "Y" (Maybe SORT, OpType, [COCOMPONENTS])
a
    (c :: SORT
c, t1 :: TERM f
t1) <- Maybe (SORT, TERM f)
forall f. Maybe (SORT, TERM f)
i1
    (_, t2 :: TERM f
t2) <- Maybe (SORT, TERM f)
forall f. Maybe (SORT, TERM f)
i2
    let p :: Range
p = SORT -> Range
posOfId SORT
c
    Named (FORMULA f) -> Maybe (Named (FORMULA f))
forall (m :: * -> *) a. Monad m => a -> m a
return (Named (FORMULA f) -> Maybe (Named (FORMULA f)))
-> Named (FORMULA f) -> Maybe (Named (FORMULA f))
forall a b. (a -> b) -> a -> b
$ [Char] -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_injective_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SORT -> [Char] -> [Char]
showId SORT
c "") (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$
       [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange ([VAR_DECL]
v1 [VAR_DECL] -> [VAR_DECL] -> [VAR_DECL]
forall a. [a] -> [a] -> [a]
++ [VAR_DECL]
v2)
       (FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation (TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation TERM f
t1 Equality
Strong TERM f
t2 Range
p) Relation
Equivalence
        (let ces :: [FORMULA f]
ces = (VAR_DECL -> VAR_DECL -> FORMULA f)
-> [VAR_DECL] -> [VAR_DECL] -> [FORMULA f]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ w1 :: VAR_DECL
w1 w2 :: VAR_DECL
w2 -> TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation
                             (VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
w1) Equality
Strong (VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
w2) Range
p) [VAR_DECL]
v1 [VAR_DECL]
v2
         in [FORMULA f] -> Range -> FORMULA f
forall f. [FORMULA f] -> Range -> FORMULA f
conjunctRange [FORMULA f]
forall f. [FORMULA f]
ces Range
p)
        Range
p) Range
p

comakeDisjoint :: [(Maybe Id, OpType, [COCOMPONENTS])] -> [Named (FORMULA f)]
comakeDisjoint :: [(Maybe SORT, OpType, [COCOMPONENTS])] -> [Named (FORMULA f)]
comakeDisjoint l :: [(Maybe SORT, OpType, [COCOMPONENTS])]
l = case [(Maybe SORT, OpType, [COCOMPONENTS])]
l of
  [] -> []
  a :: (Maybe SORT, OpType, [COCOMPONENTS])
a : as :: [(Maybe SORT, OpType, [COCOMPONENTS])]
as -> ((Maybe SORT, OpType, [COCOMPONENTS]) -> Maybe (Named (FORMULA f)))
-> [(Maybe SORT, OpType, [COCOMPONENTS])] -> [Named (FORMULA f)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((Maybe SORT, OpType, [COCOMPONENTS])
-> (Maybe SORT, OpType, [COCOMPONENTS])
-> Maybe (Named (FORMULA f))
forall f.
(Maybe SORT, OpType, [COCOMPONENTS])
-> (Maybe SORT, OpType, [COCOMPONENTS])
-> Maybe (Named (FORMULA f))
comakeDisj (Maybe SORT, OpType, [COCOMPONENTS])
a) [(Maybe SORT, OpType, [COCOMPONENTS])]
as [Named (FORMULA f)] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a] -> [a]
++ [(Maybe SORT, OpType, [COCOMPONENTS])] -> [Named (FORMULA f)]
forall f.
[(Maybe SORT, OpType, [COCOMPONENTS])] -> [Named (FORMULA f)]
comakeDisjoint [(Maybe SORT, OpType, [COCOMPONENTS])]
as

comakeDisj :: (Maybe Id, OpType, [COCOMPONENTS])
                           -> (Maybe Id, OpType, [COCOMPONENTS])
                           -> Maybe (Named (FORMULA f))
comakeDisj :: (Maybe SORT, OpType, [COCOMPONENTS])
-> (Maybe SORT, OpType, [COCOMPONENTS])
-> Maybe (Named (FORMULA f))
comakeDisj a1 :: (Maybe SORT, OpType, [COCOMPONENTS])
a1 a2 :: (Maybe SORT, OpType, [COCOMPONENTS])
a2 = do
    let (i1 :: Maybe (SORT, TERM f)
i1, v1 :: [VAR_DECL]
v1, _) = [Char]
-> (Maybe SORT, OpType, [COCOMPONENTS])
-> (Maybe (SORT, TERM f), [VAR_DECL], [(Maybe SORT, OpType)])
forall f.
[Char]
-> (Maybe SORT, OpType, [COCOMPONENTS])
-> (Maybe (SORT, TERM f), [VAR_DECL], [(Maybe SORT, OpType)])
coselForms1 "X" (Maybe SORT, OpType, [COCOMPONENTS])
a1
        (i2 :: Maybe (SORT, TERM f)
i2, v2 :: [VAR_DECL]
v2, _) = [Char]
-> (Maybe SORT, OpType, [COCOMPONENTS])
-> (Maybe (SORT, TERM f), [VAR_DECL], [(Maybe SORT, OpType)])
forall f.
[Char]
-> (Maybe SORT, OpType, [COCOMPONENTS])
-> (Maybe (SORT, TERM f), [VAR_DECL], [(Maybe SORT, OpType)])
coselForms1 "Y" (Maybe SORT, OpType, [COCOMPONENTS])
a2
    (c1 :: SORT
c1, t1 :: TERM f
t1) <- Maybe (SORT, TERM f)
forall f. Maybe (SORT, TERM f)
i1
    (c2 :: SORT
c2, t2 :: TERM f
t2) <- Maybe (SORT, TERM f)
forall f. Maybe (SORT, TERM f)
i2
    let p :: Range
p = SORT -> Range
posOfId SORT
c1 Range -> Range -> Range
`appRange` SORT -> Range
posOfId SORT
c2
    Named (FORMULA f) -> Maybe (Named (FORMULA f))
forall (m :: * -> *) a. Monad m => a -> m a
return (Named (FORMULA f) -> Maybe (Named (FORMULA f)))
-> Named (FORMULA f) -> Maybe (Named (FORMULA f))
forall a b. (a -> b) -> a -> b
$ [Char] -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_disjoint_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SORT -> [Char] -> [Char]
showId SORT
c1 "_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SORT -> [Char] -> [Char]
showId SORT
c2 "")
      (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange ([VAR_DECL]
v1 [VAR_DECL] -> [VAR_DECL] -> [VAR_DECL]
forall a. [a] -> [a] -> [a]
++ [VAR_DECL]
v2) (FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Range -> FORMULA f
Negation (TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation TERM f
t1 Equality
Strong TERM f
t2 Range
p) Range
p) Range
p

-- | return the constructor and the set of total selectors
ana_COALTERNATIVE :: SORT -> Annoted COALTERNATIVE
                -> State CSign (Maybe (Component, Set.Set Component))
ana_COALTERNATIVE :: SORT
-> Annoted COALTERNATIVE
-> State
     (Sign C_FORMULA CoCASLSign) (Maybe (Component, Set Component))
ana_COALTERNATIVE s :: SORT
s c :: Annoted COALTERNATIVE
c = case Annoted COALTERNATIVE -> COALTERNATIVE
forall a. Annoted a -> a
item Annoted COALTERNATIVE
c of
    CoSubsorts ss :: [SORT]
ss _ -> do
        (SORT -> State (Sign C_FORMULA CoCASLSign) ())
-> [SORT] -> State (Sign C_FORMULA CoCASLSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (SORT -> SORT -> State (Sign C_FORMULA CoCASLSign) ()
forall f e. SORT -> SORT -> State (Sign f e) ()
addSubsort SORT
s) [SORT]
ss
        Maybe (Component, Set Component)
-> State
     (Sign C_FORMULA CoCASLSign) (Maybe (Component, Set Component))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Component, Set Component)
forall a. Maybe a
Nothing
    ci :: COALTERNATIVE
ci -> do
        let cons :: (Maybe SORT, OpType, [COCOMPONENTS])
cons@(i :: Maybe SORT
i, ty :: OpType
ty, il :: [COCOMPONENTS]
il) = SORT -> COALTERNATIVE -> (Maybe SORT, OpType, [COCOMPONENTS])
getCoConsType SORT
s COALTERNATIVE
ci
        [([Component], [Component])]
ul <- (COCOMPONENTS
 -> State (Sign C_FORMULA CoCASLSign) ([Component], [Component]))
-> [COCOMPONENTS]
-> State (Sign C_FORMULA CoCASLSign) [([Component], [Component])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SORT
-> COCOMPONENTS
-> State (Sign C_FORMULA CoCASLSign) ([Component], [Component])
ana_COCOMPONENTS SORT
s) [COCOMPONENTS]
il
        let ts :: [Component]
ts = (([Component], [Component]) -> [Component])
-> [([Component], [Component])] -> [Component]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Component], [Component]) -> [Component]
forall a b. (a, b) -> a
fst [([Component], [Component])]
ul
        [Diagnosis] -> State (Sign C_FORMULA CoCASLSign) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State (Sign C_FORMULA CoCASLSign) ())
-> [Diagnosis] -> State (Sign C_FORMULA CoCASLSign) ()
forall a b. (a -> b) -> a -> b
$ [Component] -> [Diagnosis]
forall a. (Pretty a, GetRange a, Ord a) => [a] -> [Diagnosis]
checkUniqueness ([Component]
ts [Component] -> [Component] -> [Component]
forall a. [a] -> [a] -> [a]
++ (([Component], [Component]) -> [Component])
-> [([Component], [Component])] -> [Component]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Component], [Component]) -> [Component]
forall a b. (a, b) -> b
snd [([Component], [Component])]
ul)
        [Named (FORMULA C_FORMULA)] -> State (Sign C_FORMULA CoCASLSign) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences ([Named (FORMULA C_FORMULA)]
 -> State (Sign C_FORMULA CoCASLSign) ())
-> [Named (FORMULA C_FORMULA)]
-> State (Sign C_FORMULA CoCASLSign) ()
forall a b. (a -> b) -> a -> b
$ (Maybe SORT, OpType, [COCOMPONENTS]) -> [Named (FORMULA C_FORMULA)]
forall f.
(Maybe SORT, OpType, [COCOMPONENTS]) -> [Named (FORMULA f)]
coselForms (Maybe SORT, OpType, [COCOMPONENTS])
cons
        case Maybe SORT
i of
              Nothing -> Maybe (Component, Set Component)
-> State
     (Sign C_FORMULA CoCASLSign) (Maybe (Component, Set Component))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Component, Set Component)
forall a. Maybe a
Nothing
              Just i' :: SORT
i' -> do
                Annoted COALTERNATIVE
-> OpType -> SORT -> State (Sign C_FORMULA CoCASLSign) ()
forall a f e. Annoted a -> OpType -> SORT -> State (Sign f e) ()
addOp Annoted COALTERNATIVE
c OpType
ty SORT
i'
                Maybe (Component, Set Component)
-> State
     (Sign C_FORMULA CoCASLSign) (Maybe (Component, Set Component))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Component, Set Component)
 -> State
      (Sign C_FORMULA CoCASLSign) (Maybe (Component, Set Component)))
-> Maybe (Component, Set Component)
-> State
     (Sign C_FORMULA CoCASLSign) (Maybe (Component, Set Component))
forall a b. (a -> b) -> a -> b
$ (Component, Set Component) -> Maybe (Component, Set Component)
forall a. a -> Maybe a
Just (SORT -> OpType -> Component
Component SORT
i' OpType
ty, [Component] -> Set Component
forall a. Ord a => [a] -> Set a
Set.fromList [Component]
ts)


-- | return total and partial selectors
ana_COCOMPONENTS :: SORT -> COCOMPONENTS
               -> State CSign ([Component], [Component])
ana_COCOMPONENTS :: SORT
-> COCOMPONENTS
-> State (Sign C_FORMULA CoCASLSign) ([Component], [Component])
ana_COCOMPONENTS s :: SORT
s c :: COCOMPONENTS
c = do
    let cs :: [(SORT, OpType)]
cs = SORT -> COCOMPONENTS -> [(SORT, OpType)]
getCoCompType SORT
s COCOMPONENTS
c
    [Maybe Component]
sels <- ((SORT, OpType)
 -> State (Sign C_FORMULA CoCASLSign) (Maybe Component))
-> [(SORT, OpType)]
-> State (Sign C_FORMULA CoCASLSign) [Maybe Component]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (i :: SORT
i, ty :: OpType
ty) ->
                   do Annoted ()
-> OpType -> SORT -> State (Sign C_FORMULA CoCASLSign) ()
forall a f e. Annoted a -> OpType -> SORT -> State (Sign f e) ()
addOp (() -> Annoted ()
forall a. a -> Annoted a
emptyAnno ()) OpType
ty SORT
i
                      Maybe Component
-> State (Sign C_FORMULA CoCASLSign) (Maybe Component)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Component
 -> State (Sign C_FORMULA CoCASLSign) (Maybe Component))
-> Maybe Component
-> State (Sign C_FORMULA CoCASLSign) (Maybe Component)
forall a b. (a -> b) -> a -> b
$ Component -> Maybe Component
forall a. a -> Maybe a
Just (Component -> Maybe Component) -> Component -> Maybe Component
forall a b. (a -> b) -> a -> b
$ SORT -> OpType -> Component
Component SORT
i OpType
ty) [(SORT, OpType)]
cs
    ([Component], [Component])
-> State (Sign C_FORMULA CoCASLSign) ([Component], [Component])
forall (m :: * -> *) a. Monad m => a -> m a
return (([Component], [Component])
 -> State (Sign C_FORMULA CoCASLSign) ([Component], [Component]))
-> ([Component], [Component])
-> State (Sign C_FORMULA CoCASLSign) ([Component], [Component])
forall a b. (a -> b) -> a -> b
$ (Component -> Bool) -> [Component] -> ([Component], [Component])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (OpType -> Bool
isTotal (OpType -> Bool) -> (Component -> OpType) -> Component -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Component -> OpType
compType) ([Component] -> ([Component], [Component]))
-> [Component] -> ([Component], [Component])
forall a b. (a -> b) -> a -> b
$ [Maybe Component] -> [Component]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Component]
sels

ana_C_BASIC_ITEM
    :: Ana C_BASIC_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
ana_C_BASIC_ITEM :: Ana C_BASIC_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
ana_C_BASIC_ITEM mix :: Mix C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
mix bi :: C_BASIC_ITEM
bi = case C_BASIC_ITEM
bi of
    CoFree_datatype al :: [Annoted CODATATYPE_DECL]
al ps :: Range
ps ->
        do (Annoted CODATATYPE_DECL -> State (Sign C_FORMULA CoCASLSign) ())
-> [Annoted CODATATYPE_DECL]
-> State (Sign C_FORMULA CoCASLSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ i :: Annoted CODATATYPE_DECL
i -> case Annoted CODATATYPE_DECL -> CODATATYPE_DECL
forall a. Annoted a -> a
item Annoted CODATATYPE_DECL
i of
                  CoDatatype_decl s :: SORT
s _ _ -> SortsKind
-> Annoted CODATATYPE_DECL
-> SORT
-> State (Sign C_FORMULA CoCASLSign) ()
forall a f e. SortsKind -> Annoted a -> SORT -> State (Sign f e) ()
addSort SortsKind
NonEmptySorts Annoted CODATATYPE_DECL
i SORT
s) [Annoted CODATATYPE_DECL]
al
           (CODATATYPE_DECL -> State (Sign C_FORMULA CoCASLSign) [Component])
-> [Annoted CODATATYPE_DECL]
-> State (Sign C_FORMULA CoCASLSign) [Annoted [Component]]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM (GenKind
-> CODATATYPE_DECL -> State (Sign C_FORMULA CoCASLSign) [Component]
ana_CODATATYPE_DECL GenKind
Free) [Annoted CODATATYPE_DECL]
al
           Range -> Bool -> GenAx -> State (Sign C_FORMULA CoCASLSign) ()
toCoSortGenAx Range
ps Bool
True (GenAx -> State (Sign C_FORMULA CoCASLSign) ())
-> GenAx -> State (Sign C_FORMULA CoCASLSign) ()
forall a b. (a -> b) -> a -> b
$ [Annoted CODATATYPE_DECL] -> GenAx
getCoDataGenSig [Annoted CODATATYPE_DECL]
al
           State (Sign C_FORMULA CoCASLSign) ()
forall f e. State (Sign f e) ()
closeSubsortRel
           C_BASIC_ITEM -> State (Sign C_FORMULA CoCASLSign) C_BASIC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return C_BASIC_ITEM
bi
    CoSort_gen al :: [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
al ps :: Range
ps ->
        do (gs :: [GenAx]
gs, ul :: [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
ul) <- Ana C_SIG_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
-> Ana
     ([GenAx], [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)])
     C_BASIC_ITEM
     C_SIG_ITEM
     C_FORMULA
     CoCASLSign
ana_CoGenerated Ana C_SIG_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
ana_C_SIG_ITEM Mix C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
mix ([], [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
al)
           Range -> Bool -> GenAx -> State (Sign C_FORMULA CoCASLSign) ()
toCoSortGenAx Range
ps Bool
False (GenAx -> State (Sign C_FORMULA CoCASLSign) ())
-> GenAx -> State (Sign C_FORMULA CoCASLSign) ()
forall a b. (a -> b) -> a -> b
$ [GenAx] -> GenAx
unionGenAx [GenAx]
gs
           C_BASIC_ITEM -> State (Sign C_FORMULA CoCASLSign) C_BASIC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (C_BASIC_ITEM -> State (Sign C_FORMULA CoCASLSign) C_BASIC_ITEM)
-> C_BASIC_ITEM -> State (Sign C_FORMULA CoCASLSign) C_BASIC_ITEM
forall a b. (a -> b) -> a -> b
$ [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)] -> Range -> C_BASIC_ITEM
CoSort_gen [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
ul Range
ps

toCoSortGenAx :: Range -> Bool -> GenAx -> State CSign ()
toCoSortGenAx :: Range -> Bool -> GenAx -> State (Sign C_FORMULA CoCASLSign) ()
toCoSortGenAx ps :: Range
ps isFree :: Bool
isFree (sorts :: Set SORT
sorts, rel :: Rel SORT
rel, ops :: Set Component
ops) = do
    let sortList :: [SORT]
sortList = Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList Set SORT
sorts
        opSyms :: [OP_SYMB]
opSyms = (Component -> OP_SYMB) -> [Component] -> [OP_SYMB]
forall a b. (a -> b) -> [a] -> [b]
map (\ c :: Component
c -> let ide :: SORT
ide = Component -> SORT
compId Component
c in SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
ide
                      (OpType -> OP_TYPE
toOP_TYPE (OpType -> OP_TYPE) -> OpType -> OP_TYPE
forall a b. (a -> b) -> a -> b
$ Component -> OpType
compType Component
c) (Range -> OP_SYMB) -> Range -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ SORT -> Range
posOfId SORT
ide) ([Component] -> [OP_SYMB]) -> [Component] -> [OP_SYMB]
forall a b. (a -> b) -> a -> b
$ Set Component -> [Component]
forall a. Set a -> [a]
Set.toList Set Component
ops
        injSyms :: [OP_SYMB]
injSyms = ((SORT, SORT) -> OP_SYMB) -> [(SORT, SORT)] -> [OP_SYMB]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: SORT
s, t :: SORT
t) -> let p :: Range
p = SORT -> Range
posOfId SORT
s in
                        SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name (SORT -> SORT -> SORT
mkUniqueInjName SORT
s SORT
t)
                        (OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [SORT
s] SORT
t Range
p) Range
p) ([(SORT, SORT)] -> [OP_SYMB]) -> [(SORT, SORT)] -> [OP_SYMB]
forall a b. (a -> b) -> a -> b
$ Rel SORT -> [(SORT, SORT)]
forall a. Rel a -> [(a, a)]
Rel.toList Rel SORT
rel
    Bool
-> State (Sign C_FORMULA CoCASLSign) ()
-> State (Sign C_FORMULA CoCASLSign) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([SORT] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SORT]
sortList)
      (State (Sign C_FORMULA CoCASLSign) ()
 -> State (Sign C_FORMULA CoCASLSign) ())
-> State (Sign C_FORMULA CoCASLSign) ()
-> State (Sign C_FORMULA CoCASLSign) ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State (Sign C_FORMULA CoCASLSign) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> [Char] -> Range -> Diagnosis
Diag DiagKind
Error "missing cogenerated sort" Range
ps]
    [Named (FORMULA C_FORMULA)] -> State (Sign C_FORMULA CoCASLSign) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences [[Char] -> FORMULA C_FORMULA -> Named (FORMULA C_FORMULA)
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_cogenerated_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ([Char] -> [Char])
-> (SORT -> [Char] -> [Char]) -> [SORT] -> [Char] -> [Char]
forall a.
([Char] -> [Char])
-> (a -> [Char] -> [Char]) -> [a] -> [Char] -> [Char]
showSepList ([Char] -> [Char] -> [Char]
showString "_")
                              SORT -> [Char] -> [Char]
showId [SORT]
sortList "")
                   (FORMULA C_FORMULA -> Named (FORMULA C_FORMULA))
-> FORMULA C_FORMULA -> Named (FORMULA C_FORMULA)
forall a b. (a -> b) -> a -> b
$ C_FORMULA -> FORMULA C_FORMULA
forall f. f -> FORMULA f
ExtFORMULA (C_FORMULA -> FORMULA C_FORMULA) -> C_FORMULA -> FORMULA C_FORMULA
forall a b. (a -> b) -> a -> b
$ [SORT] -> [OP_SYMB] -> Bool -> C_FORMULA
CoSort_gen_ax [SORT]
sortList
                               ([OP_SYMB]
opSyms [OP_SYMB] -> [OP_SYMB] -> [OP_SYMB]
forall a. [a] -> [a] -> [a]
++ [OP_SYMB]
injSyms) Bool
isFree]

ana_CoGenerated :: Ana C_SIG_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
                -> Ana ([GenAx], [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)])
                   C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
ana_CoGenerated :: Ana C_SIG_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
-> Ana
     ([GenAx], [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)])
     C_BASIC_ITEM
     C_SIG_ITEM
     C_FORMULA
     CoCASLSign
ana_CoGenerated anaf :: Ana C_SIG_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
anaf mix :: Mix C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
mix (_, al :: [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
al) = do
   [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
ul <- (SIG_ITEMS C_SIG_ITEM C_FORMULA
 -> State
      (Sign C_FORMULA CoCASLSign) (SIG_ITEMS C_SIG_ITEM C_FORMULA))
-> [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
-> State
     (Sign C_FORMULA CoCASLSign)
     [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM (Min C_FORMULA CoCASLSign
-> Ana C_SIG_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
-> Mix C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
-> GenKind
-> SIG_ITEMS C_SIG_ITEM C_FORMULA
-> State
     (Sign C_FORMULA CoCASLSign) (SIG_ITEMS C_SIG_ITEM C_FORMULA)
forall f e s b.
(FormExtension f, TermExtension f) =>
Min f e
-> Ana s b s f e
-> Mix b s f e
-> GenKind
-> SIG_ITEMS s f
-> State (Sign f e) (SIG_ITEMS s f)
ana_SIG_ITEMS Min C_FORMULA CoCASLSign
minExpForm Ana C_SIG_ITEM C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
anaf Mix C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign
mix GenKind
Generated) [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
al
   ([GenAx], [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)])
-> State
     (Sign C_FORMULA CoCASLSign)
     ([GenAx], [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA) -> GenAx)
-> [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)] -> [GenAx]
forall a b. (a -> b) -> [a] -> [b]
map (SIG_ITEMS C_SIG_ITEM C_FORMULA -> GenAx
getCoGenSig (SIG_ITEMS C_SIG_ITEM C_FORMULA -> GenAx)
-> (Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)
    -> SIG_ITEMS C_SIG_ITEM C_FORMULA)
-> Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)
-> GenAx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)
-> SIG_ITEMS C_SIG_ITEM C_FORMULA
forall a. Annoted a -> a
item) [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
ul, [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
ul)

getCoGenSig :: SIG_ITEMS C_SIG_ITEM C_FORMULA -> GenAx
getCoGenSig :: SIG_ITEMS C_SIG_ITEM C_FORMULA -> GenAx
getCoGenSig si :: SIG_ITEMS C_SIG_ITEM C_FORMULA
si = case SIG_ITEMS C_SIG_ITEM C_FORMULA
si of
      Sort_items _ al :: [Annoted (SORT_ITEM C_FORMULA)]
al _ -> [GenAx] -> GenAx
unionGenAx ([GenAx] -> GenAx) -> [GenAx] -> GenAx
forall a b. (a -> b) -> a -> b
$ (Annoted (SORT_ITEM C_FORMULA) -> GenAx)
-> [Annoted (SORT_ITEM C_FORMULA)] -> [GenAx]
forall a b. (a -> b) -> [a] -> [b]
map (SORT_ITEM C_FORMULA -> GenAx
forall f. SORT_ITEM f -> GenAx
getGenSorts (SORT_ITEM C_FORMULA -> GenAx)
-> (Annoted (SORT_ITEM C_FORMULA) -> SORT_ITEM C_FORMULA)
-> Annoted (SORT_ITEM C_FORMULA)
-> GenAx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (SORT_ITEM C_FORMULA) -> SORT_ITEM C_FORMULA
forall a. Annoted a -> a
item) [Annoted (SORT_ITEM C_FORMULA)]
al
      Op_items al :: [Annoted (OP_ITEM C_FORMULA)]
al _ -> (Set SORT
forall a. Set a
Set.empty, Rel SORT
forall a. Rel a
Rel.empty,
                           [Set Component] -> Set Component
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ((Annoted (OP_ITEM C_FORMULA) -> Set Component)
-> [Annoted (OP_ITEM C_FORMULA)] -> [Set Component]
forall a b. (a -> b) -> [a] -> [b]
map (OP_ITEM C_FORMULA -> Set Component
forall f. OP_ITEM f -> Set Component
getOps (OP_ITEM C_FORMULA -> Set Component)
-> (Annoted (OP_ITEM C_FORMULA) -> OP_ITEM C_FORMULA)
-> Annoted (OP_ITEM C_FORMULA)
-> Set Component
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (OP_ITEM C_FORMULA) -> OP_ITEM C_FORMULA
forall a. Annoted a -> a
item) [Annoted (OP_ITEM C_FORMULA)]
al))
      Datatype_items _ dl :: [Annoted DATATYPE_DECL]
dl _ -> [Annoted DATATYPE_DECL] -> GenAx
getDataGenSig [Annoted DATATYPE_DECL]
dl
      Ext_SIG_ITEMS (CoDatatype_items dl :: [Annoted CODATATYPE_DECL]
dl _) -> [Annoted CODATATYPE_DECL] -> GenAx
getCoDataGenSig [Annoted CODATATYPE_DECL]
dl
      _ -> GenAx
emptyGenAx

getCoDataGenSig :: [Annoted CODATATYPE_DECL] -> GenAx
getCoDataGenSig :: [Annoted CODATATYPE_DECL] -> GenAx
getCoDataGenSig dl :: [Annoted CODATATYPE_DECL]
dl =
    let get_sel :: (SORT, COALTERNATIVE) -> [(SORT, OpType)]
get_sel (s :: SORT
s, a :: COALTERNATIVE
a) = case COALTERNATIVE
a of
          CoSubsorts _ _ -> []
          Co_construct _ _ l :: [COCOMPONENTS]
l _ -> (COCOMPONENTS -> [(SORT, OpType)])
-> [COCOMPONENTS] -> [(SORT, OpType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SORT -> COCOMPONENTS -> [(SORT, OpType)]
getCoCompType SORT
s) [COCOMPONENTS]
l
        alts :: [(SORT, COALTERNATIVE)]
alts = (Annoted CODATATYPE_DECL -> [(SORT, COALTERNATIVE)])
-> [Annoted CODATATYPE_DECL] -> [(SORT, COALTERNATIVE)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((\ (CoDatatype_decl s :: SORT
s al :: [Annoted COALTERNATIVE]
al _) ->
                       (Annoted COALTERNATIVE -> (SORT, COALTERNATIVE))
-> [Annoted COALTERNATIVE] -> [(SORT, COALTERNATIVE)]
forall a b. (a -> b) -> [a] -> [b]
map (\ a :: Annoted COALTERNATIVE
a -> (SORT
s, Annoted COALTERNATIVE -> COALTERNATIVE
forall a. Annoted a -> a
item Annoted COALTERNATIVE
a)) [Annoted COALTERNATIVE]
al) (CODATATYPE_DECL -> [(SORT, COALTERNATIVE)])
-> (Annoted CODATATYPE_DECL -> CODATATYPE_DECL)
-> Annoted CODATATYPE_DECL
-> [(SORT, COALTERNATIVE)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted CODATATYPE_DECL -> CODATATYPE_DECL
forall a. Annoted a -> a
item) [Annoted CODATATYPE_DECL]
dl
        sorts :: [SORT]
sorts = ((SORT, COALTERNATIVE) -> SORT)
-> [(SORT, COALTERNATIVE)] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, COALTERNATIVE) -> SORT
forall a b. (a, b) -> a
fst [(SORT, COALTERNATIVE)]
alts
        (realAlts :: [(SORT, COALTERNATIVE)]
realAlts, subs :: [(SORT, COALTERNATIVE)]
subs) = ((SORT, COALTERNATIVE) -> Bool)
-> [(SORT, COALTERNATIVE)]
-> ([(SORT, COALTERNATIVE)], [(SORT, COALTERNATIVE)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (COALTERNATIVE -> Bool
isCoConsAlt (COALTERNATIVE -> Bool)
-> ((SORT, COALTERNATIVE) -> COALTERNATIVE)
-> (SORT, COALTERNATIVE)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SORT, COALTERNATIVE) -> COALTERNATIVE
forall a b. (a, b) -> b
snd) [(SORT, COALTERNATIVE)]
alts
        sels :: [Component]
sels = ((SORT, OpType) -> Component) -> [(SORT, OpType)] -> [Component]
forall a b. (a -> b) -> [a] -> [b]
map ((SORT -> OpType -> Component) -> (SORT, OpType) -> Component
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SORT -> OpType -> Component
Component) ([(SORT, OpType)] -> [Component])
-> [(SORT, OpType)] -> [Component]
forall a b. (a -> b) -> a -> b
$ ((SORT, COALTERNATIVE) -> [(SORT, OpType)])
-> [(SORT, COALTERNATIVE)] -> [(SORT, OpType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SORT, COALTERNATIVE) -> [(SORT, OpType)]
get_sel [(SORT, COALTERNATIVE)]
realAlts
        rel :: Rel SORT
rel = ((SORT, COALTERNATIVE) -> Rel SORT -> Rel SORT)
-> Rel SORT -> [(SORT, COALTERNATIVE)] -> Rel SORT
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (t :: SORT
t, a :: COALTERNATIVE
a) r :: Rel SORT
r ->
                     (SORT -> Rel SORT -> Rel SORT) -> Rel SORT -> [SORT] -> Rel SORT
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (SORT -> SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> a -> Rel a -> Rel a
`Rel.insertDiffPair` SORT
t) Rel SORT
r ([SORT] -> Rel SORT) -> [SORT] -> Rel SORT
forall a b. (a -> b) -> a -> b
$ COALTERNATIVE -> [SORT]
getCoSubsorts COALTERNATIVE
a)
               Rel SORT
forall a. Rel a
Rel.empty [(SORT, COALTERNATIVE)]
subs
        in ([SORT] -> Set SORT
forall a. Ord a => [a] -> Set a
Set.fromList [SORT]
sorts, Rel SORT
rel, [Component] -> Set Component
forall a. Ord a => [a] -> Set a
Set.fromList [Component]
sels)