{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/CASL2TopSort.hs
Copyright   :  (c) Klaus Luettich, Uni Bremen 2002-2004
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

Coding out subsorting into unary predicates.
   New concept for proving Ontologies.

generatedness via non-injective datatype constructors
(i.e. proper data constructors) is simply ignored

total functions my become partial because i.e. division is total
for a second non-zero argument but partial otherwise.

partial functions remain partial unless they fall to together
with an overloaded total function
-}

module Comorphisms.CASL2TopSort (CASL2TopSort (..)) where

import Data.Ord
import Data.Maybe
import Data.List

import Logic.Logic
import Logic.Comorphism

import Common.AS_Annotation
import Common.Id
import Common.ProofTree
import Common.Result
import qualified Common.Lib.Rel as Rel
import qualified Common.Lib.MapSet as MapSet

-- CASL
import CASL.Logic_CASL
import CASL.AS_Basic_CASL
import CASL.Fold
import CASL.Sign
import CASL.StaticAna (sortsOfArgs)
import CASL.Morphism
import CASL.Sublogic as SL

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

-- | The identity of the comorphism
data CASL2TopSort = CASL2TopSort deriving Int -> CASL2TopSort -> ShowS
[CASL2TopSort] -> ShowS
CASL2TopSort -> String
(Int -> CASL2TopSort -> ShowS)
-> (CASL2TopSort -> String)
-> ([CASL2TopSort] -> ShowS)
-> Show CASL2TopSort
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CASL2TopSort] -> ShowS
$cshowList :: [CASL2TopSort] -> ShowS
show :: CASL2TopSort -> String
$cshow :: CASL2TopSort -> String
showsPrec :: Int -> CASL2TopSort -> ShowS
$cshowsPrec :: Int -> CASL2TopSort -> ShowS
Show

instance Language CASL2TopSort where
  language_name :: CASL2TopSort -> String
language_name CASL2TopSort = "CASL2PCFOLTopSort"

instance Comorphism CASL2TopSort
               CASL CASL_Sublogics
               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CASLSign
               CASLMor
               Symbol RawSymbol ProofTree
               CASL CASL_Sublogics
               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CASLSign
               CASLMor
               Symbol RawSymbol ProofTree where
    sourceLogic :: CASL2TopSort -> CASL
sourceLogic CASL2TopSort = CASL
CASL
    sourceSublogic :: CASL2TopSort -> CASL_Sublogics
sourceSublogic CASL2TopSort = CASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.caslTop
        { sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
LocFilSub
        , cons_features :: SortGenerationFeatures
cons_features = SortGenerationFeatures
emptyMapConsFeature }
    targetLogic :: CASL2TopSort -> CASL
targetLogic CASL2TopSort = CASL
CASL
    mapSublogic :: CASL2TopSort -> CASL_Sublogics -> Maybe CASL_Sublogics
mapSublogic CASL2TopSort sub :: CASL_Sublogics
sub =
        if CASL_Sublogics
sub CASL_Sublogics -> CASL_Sublogics -> Bool
forall l. SemiLatticeWithTop l => l -> l -> Bool
`isSubElem` CASL2TopSort -> CASL_Sublogics
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sublogics1
sourceSublogic CASL2TopSort
CASL2TopSort
        then CASL_Sublogics -> Maybe CASL_Sublogics
forall a. a -> Maybe a
Just (CASL_Sublogics -> Maybe CASL_Sublogics)
-> CASL_Sublogics -> Maybe CASL_Sublogics
forall a b. (a -> b) -> a -> b
$
         CASL_Sublogics
sub { sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
NoSub      -- subsorting is coded out
             , cons_features :: SortGenerationFeatures
cons_features = SortGenerationFeatures
NoSortGen -- special Sort_gen_ax is coded out
             , which_logic :: CASL_Formulas
which_logic = CASL_Formulas -> CASL_Formulas -> CASL_Formulas
forall a. Ord a => a -> a -> a
max CASL_Formulas
Horn (CASL_Sublogics -> CASL_Formulas
forall a. CASL_SL a -> CASL_Formulas
which_logic CASL_Sublogics
sub)
             , has_eq :: Bool
has_eq = Bool
True             {- was in the original targetLogic
               may be avoided through predications of sort-preds
               with the result terms of functions instead of formulas like:
               forall x : T . bot = x => a(x)
               better: . a(bot) -}
             , has_pred :: Bool
has_pred = Bool
True
             , has_part :: Bool
has_part = Bool
True }
             {- subsorting is coded out and
             special Sort_gen_ax are coded out -}
        else Maybe CASL_Sublogics
forall a. Maybe a
Nothing

    map_theory :: CASL2TopSort
-> (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
map_theory CASL2TopSort = (CASLSign -> Result (CASLSign, [Named CASLFORMULA]))
-> (CASLSign -> CASLFORMULA -> Result CASLFORMULA)
-> (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) sign1 sign2 sentence2 sentence1.
Monad m =>
(sign1 -> m (sign2, [Named sentence2]))
-> (sign1 -> sentence1 -> m sentence2)
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
mkTheoryMapping CASLSign -> Result (CASLSign, [Named CASLFORMULA])
forall e. Sign () e -> Result (Sign () e, [Named CASLFORMULA])
transSig CASLSign -> CASLFORMULA -> Result CASLFORMULA
forall f e. Sign f e -> FORMULA f -> Result (FORMULA f)
transSen
    map_morphism :: CASL2TopSort -> CASLMor -> Result CASLMor
map_morphism CASL2TopSort mor :: CASLMor
mor = do
        let trSig :: Sign () e -> Result (Sign () e)
trSig = ((Sign () e, [Named CASLFORMULA]) -> Sign () e)
-> Result (Sign () e, [Named CASLFORMULA]) -> Result (Sign () e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sign () e, [Named CASLFORMULA]) -> Sign () e
forall a b. (a, b) -> a
fst (Result (Sign () e, [Named CASLFORMULA]) -> Result (Sign () e))
-> (Sign () e -> Result (Sign () e, [Named CASLFORMULA]))
-> Sign () e
-> Result (Sign () e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign () e -> Result (Sign () e, [Named CASLFORMULA])
forall e. Sign () e -> Result (Sign () e, [Named CASLFORMULA])
transSig
        CASLSign
sigSour <- CASLSign -> Result CASLSign
forall e. Sign () e -> Result (Sign () e)
trSig (CASLSign -> Result CASLSign) -> CASLSign -> Result CASLSign
forall a b. (a -> b) -> a -> b
$ CASLMor -> CASLSign
forall f e m. Morphism f e m -> Sign f e
msource CASLMor
mor
        CASLSign
sigTarg <- CASLSign -> Result CASLSign
forall e. Sign () e -> Result (Sign () e)
trSig (CASLSign -> Result CASLSign) -> CASLSign -> Result CASLSign
forall a b. (a -> b) -> a -> b
$ CASLMor -> CASLSign
forall f e m. Morphism f e m -> Sign f e
mtarget CASLMor
mor
        CASLMor -> Result CASLMor
forall (m :: * -> *) a. Monad m => a -> m a
return CASLMor
mor
          { msource :: CASLSign
msource = CASLSign
sigSour
          , mtarget :: CASLSign
mtarget = CASLSign
sigTarg }
    map_sentence :: CASL2TopSort -> CASLSign -> CASLFORMULA -> Result CASLFORMULA
map_sentence CASL2TopSort = CASLSign -> CASLFORMULA -> Result CASLFORMULA
forall f e. Sign f e -> FORMULA f -> Result (FORMULA f)
transSen
    map_symbol :: CASL2TopSort -> CASLSign -> Symbol -> Set Symbol
map_symbol CASL2TopSort _ = Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Symbol -> Set Symbol)
-> (Symbol -> Symbol) -> Symbol -> Set Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
forall a. a -> a
id
    has_model_expansion :: CASL2TopSort -> Bool
has_model_expansion CASL2TopSort = Bool
True

data PredInfo = PredInfo { PredInfo -> SORT
topSortPI :: SORT
                         , PredInfo -> Set SORT
directSuperSortsPI :: Set.Set SORT
                         , PredInfo -> SORT
predicatePI :: PRED_NAME
                         } deriving Int -> PredInfo -> ShowS
[PredInfo] -> ShowS
PredInfo -> String
(Int -> PredInfo -> ShowS)
-> (PredInfo -> String) -> ([PredInfo] -> ShowS) -> Show PredInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PredInfo] -> ShowS
$cshowList :: [PredInfo] -> ShowS
show :: PredInfo -> String
$cshow :: PredInfo -> String
showsPrec :: Int -> PredInfo -> ShowS
$cshowsPrec :: Int -> PredInfo -> ShowS
Show

type SubSortMap = Map.Map SORT PredInfo

generateSubSortMap :: Rel.Rel SORT -> PredMap -> SubSortMap
generateSubSortMap :: Rel SORT -> PredMap -> SubSortMap
generateSubSortMap sortRels :: Rel SORT
sortRels pMap :: PredMap
pMap =
    let disAmbMap :: Map k PredInfo -> Map k PredInfo
disAmbMap = (PredInfo -> PredInfo) -> Map k PredInfo -> Map k PredInfo
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map PredInfo -> PredInfo
disAmbPred
        disAmbPred :: PredInfo -> PredInfo
disAmbPred v :: PredInfo
v = let pn :: SORT
pn = PredInfo -> SORT
predicatePI PredInfo
v in
          case (SORT -> Bool) -> [SORT] -> [SORT]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` PredMap -> Set SORT
forall a b. MapSet a b -> Set a
MapSet.keysSet PredMap
pMap)
                   ([SORT] -> [SORT]) -> [SORT] -> [SORT]
forall a b. (a -> b) -> a -> b
$ SORT
pn SORT -> [SORT] -> [SORT]
forall a. a -> [a] -> [a]
: (Int -> SORT) -> [Int] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (\x :: Int
x -> SORT -> String -> SORT
appendString (PredInfo -> SORT
predicatePI PredInfo
v) (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
x) 
                          [1::Int ..] of
            n :: SORT
n : _ -> PredInfo
v { predicatePI :: SORT
predicatePI = SORT
n }
            [] -> String -> PredInfo
forall a. HasCallStack => String -> a
error "generateSubSortMap"
        mR :: Set SORT
mR = ([Set SORT] -> Set SORT
forall a. Ord a => [Set a] -> Set a
Rel.flatSet ([Set SORT] -> Set SORT)
-> (Set SORT -> [Set SORT]) -> Set SORT -> Set SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
              (SORT -> SORT -> Bool) -> Set SORT -> [Set SORT]
forall a. Ord a => (a -> a -> Bool) -> Set a -> [Set a]
Rel.partSet (\ x :: SORT
x y :: SORT
y -> SORT -> SORT -> Rel SORT -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.member SORT
x SORT
y Rel SORT
sortRels Bool -> Bool -> Bool
&&
                                    SORT -> SORT -> Rel SORT -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.member SORT
y SORT
x Rel SORT
sortRels))
             (Rel SORT -> Set SORT
forall a. Ord a => Rel a -> Set a
Rel.mostRight Rel SORT
sortRels)
        toPredInfo :: SORT -> Set SORT -> PredInfo
toPredInfo k :: SORT
k e :: Set SORT
e =
            let ts :: SORT
ts = case (SORT -> Bool) -> [SORT] -> [SORT]
forall a. (a -> Bool) -> [a] -> [a]
filter ((SORT -> Rel SORT -> Bool) -> Rel SORT -> SORT -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (SORT -> SORT -> Rel SORT -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.member SORT
k) Rel SORT
sortRels)
                     ([SORT] -> [SORT]) -> [SORT] -> [SORT]
forall a b. (a -> b) -> a -> b
$ Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList Set SORT
mR of
                     [x :: SORT
x] -> SORT
x
                     _ -> String -> SORT
forall a. HasCallStack => String -> a
error "CASL2TopSort.generateSubSortMap.toPredInfo"
            in PredInfo :: SORT -> Set SORT -> SORT -> PredInfo
PredInfo { topSortPI :: SORT
topSortPI = SORT
ts
                        , directSuperSortsPI :: Set SORT
directSuperSortsPI = Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set SORT
e Set SORT
mR
                        , predicatePI :: SORT
predicatePI = SORT
k }
        initMap :: SubSortMap
initMap = (SORT -> PredInfo -> Bool) -> SubSortMap -> SubSortMap
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\ k :: SORT
k _ -> 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
k Set SORT
mR)
            ((SORT -> Set SORT -> PredInfo) -> Map SORT (Set SORT) -> SubSortMap
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey SORT -> Set SORT -> PredInfo
toPredInfo
                   (Rel SORT -> Map SORT (Set SORT)
forall a. Rel a -> Map a (Set a)
Rel.toMap (Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.intransKernel Rel SORT
sortRels)))
    in SubSortMap -> SubSortMap
forall k. Map k PredInfo -> Map k PredInfo
disAmbMap SubSortMap
initMap

{- | Finds Top-sort(s) and transforms for each top-sort all subsorts
into unary predicates. All predicates typed with subsorts are now
typed with the top-sort and axioms reflecting the typing are
generated. The operations are treated analogous. Axioms are
generated that each generated unary predicate must hold on at least
one element of the top-sort. -}

transSig :: Sign () e -> Result (Sign () e, [Named (FORMULA ())])
transSig :: Sign () e -> Result (Sign () e, [Named CASLFORMULA])
transSig sig :: Sign () e
sig = (Sign () e, [Named CASLFORMULA])
-> Result (Sign () e, [Named CASLFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return
  ((Sign () e, [Named CASLFORMULA])
 -> Result (Sign () e, [Named CASLFORMULA]))
-> (Sign () e, [Named CASLFORMULA])
-> Result (Sign () e, [Named CASLFORMULA])
forall a b. (a -> b) -> a -> b
$ let sortRels :: Rel SORT
sortRels = Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.rmNullSets (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ Sign () e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign () e
sig in
    if Rel SORT -> Bool
forall a. Rel a -> Bool
Rel.nullKeys Rel SORT
sortRels then (Sign () e
sig, []) else
    let subSortMap :: SubSortMap
subSortMap = Rel SORT -> PredMap -> SubSortMap
generateSubSortMap Rel SORT
sortRels (Sign () e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign () e
sig)
        newOpMap :: OpMap
newOpMap = Rel SORT -> SubSortMap -> OpMap -> OpMap
transOpMap Rel SORT
sortRels SubSortMap
subSortMap (Sign () e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign () e
sig)
        newAssOpMap0 :: OpMap
newAssOpMap0 = Rel SORT -> SubSortMap -> OpMap -> OpMap
transOpMap Rel SORT
sortRels SubSortMap
subSortMap (Sign () e -> OpMap
forall f e. Sign f e -> OpMap
assocOps Sign () e
sig)
        axs :: [Named CASLFORMULA]
axs = SubSortMap -> PredMap -> OpMap -> [Named CASLFORMULA]
generateAxioms SubSortMap
subSortMap (Sign () e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign () e
sig) OpMap
newOpMap
        newPreds :: Map k PredInfo -> PredMap
newPreds = (PredInfo -> PredMap -> PredMap)
-> PredMap -> [PredInfo] -> PredMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ pI :: PredInfo
pI -> SORT -> PredType -> PredMap -> PredMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert (PredInfo -> SORT
predicatePI PredInfo
pI)
                          (PredType -> PredMap -> PredMap) -> PredType -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ [SORT] -> PredType
PredType [PredInfo -> SORT
topSortPI PredInfo
pI])
                    PredMap
forall a b. MapSet a b
MapSet.empty ([PredInfo] -> PredMap)
-> (Map k PredInfo -> [PredInfo]) -> Map k PredInfo -> PredMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map k PredInfo -> [PredInfo]
forall k a. Map k a -> [a]
Map.elems
        newPredMap :: PredMap
newPredMap = PredMap -> PredMap -> PredMap
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.union (SubSortMap -> PredMap -> PredMap
transPredMap SubSortMap
subSortMap
                  (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ Sign () e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign () e
sig) (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ SubSortMap -> PredMap
forall k. Map k PredInfo -> PredMap
newPreds SubSortMap
subSortMap
    in (Sign () e
sig
        { sortRel :: Rel SORT
sortRel = Set SORT -> Rel SORT
forall a. Ord a => Set a -> Rel a
Rel.fromKeysSet
            (Set SORT -> Rel SORT) -> Set SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ [SORT] -> Set SORT
forall a. Ord a => [a] -> Set a
Set.fromList ((PredInfo -> SORT) -> [PredInfo] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map PredInfo -> SORT
topSortPI ([PredInfo] -> [SORT]) -> [PredInfo] -> [SORT]
forall a b. (a -> b) -> a -> b
$ SubSortMap -> [PredInfo]
forall k a. Map k a -> [a]
Map.elems SubSortMap
subSortMap)
              Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` (Sign () e -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet Sign () e
sig Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` SubSortMap -> Set SORT
forall k a. Map k a -> Set k
Map.keysSet SubSortMap
subSortMap)
        , opMap :: OpMap
opMap = OpMap
newOpMap
        , assocOps :: OpMap
assocOps = OpMap -> OpMap -> OpMap
interOpMapSet OpMap
newAssOpMap0 OpMap
newOpMap
        , predMap :: PredMap
predMap = PredMap
newPredMap
        }, [Named CASLFORMULA]
axs [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ SubSortMap -> Rel SORT -> [Named CASLFORMULA]
symmetryAxioms SubSortMap
subSortMap Rel SORT
sortRels)

transPredMap :: SubSortMap -> PredMap -> PredMap
transPredMap :: SubSortMap -> PredMap -> PredMap
transPredMap subSortMap :: SubSortMap
subSortMap = (PredType -> PredType) -> PredMap -> PredMap
forall b c a.
(Ord b, Ord c) =>
(b -> c) -> MapSet a b -> MapSet a c
MapSet.map PredType -> PredType
transType
    where transType :: PredType -> PredType
transType t :: PredType
t = PredType
t
            { predArgs :: [SORT]
predArgs = (SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (SubSortMap -> SORT -> SORT
lkupTop SubSortMap
subSortMap) ([SORT] -> [SORT]) -> [SORT] -> [SORT]
forall a b. (a -> b) -> a -> b
$ PredType -> [SORT]
predArgs PredType
t }

transOpMap :: Rel.Rel SORT -> SubSortMap -> OpMap -> OpMap
transOpMap :: Rel SORT -> SubSortMap -> OpMap -> OpMap
transOpMap sRel :: Rel SORT
sRel subSortMap :: SubSortMap
subSortMap = Bool -> OpMap -> OpMap
rmOrAddPartsMap Bool
True (OpMap -> OpMap) -> (OpMap -> OpMap) -> OpMap -> OpMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OpType -> OpType) -> OpMap -> OpMap
forall b c a.
(Ord b, Ord c) =>
(b -> c) -> MapSet a b -> MapSet a c
MapSet.map OpType -> OpType
transType
    where
          transType :: OpType -> OpType
transType t :: OpType
t =
              let args :: [SORT]
args = OpType -> [SORT]
opArgs OpType
t
                  lkp :: SORT -> SORT
lkp = SubSortMap -> SORT -> SORT
lkupTop SubSortMap
subSortMap
                  newArgs :: [SORT]
newArgs = (SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> SORT
lkp [SORT]
args
                  kd :: OpKind
kd = OpType -> OpKind
opKind OpType
t
              in -- make function partial if argument sorts are subsorts
              OpType
t { opArgs :: [SORT]
opArgs = (SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> SORT
lkp ([SORT] -> [SORT]) -> [SORT] -> [SORT]
forall a b. (a -> b) -> a -> b
$ OpType -> [SORT]
opArgs OpType
t
                , opRes :: SORT
opRes = SORT -> SORT
lkp (SORT -> SORT) -> SORT -> SORT
forall a b. (a -> b) -> a -> b
$ OpType -> SORT
opRes OpType
t
                , opKind :: OpKind
opKind = if OpKind
kd OpKind -> OpKind -> Bool
forall a. Eq a => a -> a -> Bool
== OpKind
Total Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((SORT -> SORT -> Bool) -> [SORT] -> [SORT] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
                           (\ a :: SORT
a na :: SORT
na -> SORT
a SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
na Bool -> Bool -> Bool
|| SORT -> SORT -> Rel SORT -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.member SORT
na SORT
a Rel SORT
sRel)
                           [SORT]
args [SORT]
newArgs) then OpKind
kd else OpKind
Partial }

procOpMapping :: SubSortMap -> OP_NAME -> Set.Set OpType
  -> [Named (FORMULA ())] -> [Named (FORMULA ())]
procOpMapping :: SubSortMap
-> SORT -> Set OpType -> [Named CASLFORMULA] -> [Named CASLFORMULA]
procOpMapping subSortMap :: SubSortMap
subSortMap opName :: SORT
opName =
  [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
(++) ([Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA])
-> (Set OpType -> [Named CASLFORMULA])
-> Set OpType
-> [Named CASLFORMULA]
-> [Named CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([SORT]
 -> (OpKind, Set [Maybe SORT])
 -> [Named CASLFORMULA]
 -> [Named CASLFORMULA])
-> [Named CASLFORMULA]
-> Map [SORT] (OpKind, Set [Maybe SORT])
-> [Named CASLFORMULA]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey [SORT]
-> (OpKind, Set [Maybe SORT])
-> [Named CASLFORMULA]
-> [Named CASLFORMULA]
procProfMapOpMapping [] (Map [SORT] (OpKind, Set [Maybe SORT]) -> [Named CASLFORMULA])
-> (Set OpType -> Map [SORT] (OpKind, Set [Maybe SORT]))
-> Set OpType
-> [Named CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SubSortMap -> Set OpType -> Map [SORT] (OpKind, Set [Maybe SORT])
mkProfMapOp SubSortMap
subSortMap
  where
    procProfMapOpMapping :: [SORT] -> (OpKind, Set.Set [Maybe PRED_NAME])
                         -> [Named (FORMULA ())] -> [Named (FORMULA ())]
    procProfMapOpMapping :: [SORT]
-> (OpKind, Set [Maybe SORT])
-> [Named CASLFORMULA]
-> [Named CASLFORMULA]
procProfMapOpMapping sl :: [SORT]
sl (kind :: OpKind
kind, spl :: Set [Maybe SORT]
spl) = String
-> ([VAR_DECL] -> CASLFORMULA)
-> [SORT]
-> Set [Maybe SORT]
-> [Named CASLFORMULA]
-> [Named CASLFORMULA]
forall f.
String
-> ([VAR_DECL] -> FORMULA f)
-> [SORT]
-> Set [Maybe SORT]
-> [Named (FORMULA f)]
-> [Named (FORMULA f)]
genArgRest
        (String -> SORT -> Int -> String
forall a. Show a => String -> a -> Int -> String
genSenName "o" SORT
opName (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ [SORT] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SORT]
sl) (OpKind -> SORT -> [VAR_DECL] -> CASLFORMULA
forall f. OpKind -> SORT -> [VAR_DECL] -> FORMULA f
genOpEquation OpKind
kind SORT
opName) [SORT]
sl Set [Maybe SORT]
spl

mkSimpleQualPred :: PRED_NAME -> SORT -> PRED_SYMB
mkSimpleQualPred :: SORT -> SORT -> PRED_SYMB
mkSimpleQualPred symS :: SORT
symS ts :: SORT
ts = SORT -> PRED_TYPE -> PRED_SYMB
mkQualPred SORT
symS (PRED_TYPE -> PRED_SYMB) -> PRED_TYPE -> PRED_SYMB
forall a b. (a -> b) -> a -> b
$ [SORT] -> Range -> PRED_TYPE
Pred_type [SORT
ts] Range
nullRange

symmetryAxioms :: SubSortMap -> Rel.Rel SORT -> [Named (FORMULA ())]
symmetryAxioms :: SubSortMap -> Rel SORT -> [Named CASLFORMULA]
symmetryAxioms ssMap :: SubSortMap
ssMap sortRels :: Rel SORT
sortRels =
    let symSets :: [Set SORT]
symSets = Rel SORT -> [Set SORT]
forall a. Ord a => Rel a -> [Set a]
Rel.sccOfClosure Rel SORT
sortRels
        toAxioms :: Set SORT -> [SenAttr (FORMULA f) String]
toAxioms = (SORT -> [SenAttr (FORMULA f) String])
-> [SORT] -> [SenAttr (FORMULA f) String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
          (\ s :: SORT
s ->
            let ts :: SORT
ts = SubSortMap -> SORT -> SORT
lkupTop SubSortMap
ssMap SORT
s
                symS :: SORT
symS = SubSortMap -> SORT -> SORT
lkupPred SubSortMap
ssMap SORT
s
                psy :: PRED_SYMB
psy = SORT -> SORT -> PRED_SYMB
mkSimpleQualPred SORT
symS SORT
ts
                vd :: VAR_DECL
vd = String -> SORT -> VAR_DECL
mkVarDeclStr "x" SORT
ts
                vt :: TERM f
vt = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
vd
            in if SORT
ts SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
s then [] else
                   [String -> FORMULA f -> SenAttr (FORMULA f) String
forall a s. a -> s -> SenAttr s a
makeNamed (SORT -> String
forall a. Show a => a -> String
show SORT
ts String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_symmetric_with_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show SORT
symS)
                   (FORMULA f -> SenAttr (FORMULA f) String)
-> FORMULA f -> SenAttr (FORMULA f) String
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL
vd] (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ PRED_SYMB -> [TERM f] -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
psy [TERM f
forall f. TERM f
vt]]
          ) ([SORT] -> [SenAttr (FORMULA f) String])
-> (Set SORT -> [SORT]) -> Set SORT -> [SenAttr (FORMULA f) String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList
    in (Set SORT -> [Named CASLFORMULA])
-> [Set SORT] -> [Named CASLFORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Set SORT -> [Named CASLFORMULA]
forall f. Set SORT -> [SenAttr (FORMULA f) String]
toAxioms [Set SORT]
symSets

generateAxioms :: SubSortMap -> PredMap -> OpMap -> [Named (FORMULA ())]
generateAxioms :: SubSortMap -> PredMap -> OpMap -> [Named CASLFORMULA]
generateAxioms subSortMap :: SubSortMap
subSortMap pMap :: PredMap
pMap oMap :: OpMap
oMap = [Named CASLFORMULA]
forall f. [SenAttr (FORMULA f) String]
hi_axs [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
forall f. [SenAttr (FORMULA f) String]
p_axs [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
axs
    where -- generate argument restrictions for operations
          axs :: [Named CASLFORMULA]
axs = (SORT -> Set OpType -> [Named CASLFORMULA] -> [Named CASLFORMULA])
-> [Named CASLFORMULA]
-> Map SORT (Set OpType)
-> [Named CASLFORMULA]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (SubSortMap
-> SORT -> Set OpType -> [Named CASLFORMULA] -> [Named CASLFORMULA]
procOpMapping SubSortMap
subSortMap) []
                (Map SORT (Set OpType) -> [Named CASLFORMULA])
-> Map SORT (Set OpType) -> [Named CASLFORMULA]
forall a b. (a -> b) -> a -> b
$ OpMap -> Map SORT (Set OpType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap OpMap
oMap
          p_axs :: [Named (FORMULA f)]
p_axs =
          -- generate argument restrictions for predicates
           (SORT
 -> Set PredType -> [Named (FORMULA f)] -> [Named (FORMULA f)])
-> [Named (FORMULA f)]
-> Map SORT (Set PredType)
-> [Named (FORMULA f)]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ pName :: SORT
pName ->
              [Named (FORMULA f)] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a] -> [a]
(++) ([Named (FORMULA f)] -> [Named (FORMULA f)] -> [Named (FORMULA f)])
-> (Set PredType -> [Named (FORMULA f)])
-> Set PredType
-> [Named (FORMULA f)]
-> [Named (FORMULA f)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([SORT]
 -> Set [Maybe SORT] -> [Named (FORMULA f)] -> [Named (FORMULA f)])
-> [Named (FORMULA f)]
-> Map [SORT] (Set [Maybe SORT])
-> [Named (FORMULA f)]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey
                             (\ sl :: [SORT]
sl -> String
-> ([VAR_DECL] -> FORMULA f)
-> [SORT]
-> Set [Maybe SORT]
-> [Named (FORMULA f)]
-> [Named (FORMULA f)]
forall f.
String
-> ([VAR_DECL] -> FORMULA f)
-> [SORT]
-> Set [Maybe SORT]
-> [Named (FORMULA f)]
-> [Named (FORMULA f)]
genArgRest
                                      (String -> SORT -> Int -> String
forall a. Show a => String -> a -> Int -> String
genSenName "p" SORT
pName (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ [SORT] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SORT]
sl)
                                      (SORT -> [VAR_DECL] -> FORMULA f
forall f. SORT -> [VAR_DECL] -> FORMULA f
genPredication SORT
pName)
                                      [SORT]
sl)
                                    [] (Map [SORT] (Set [Maybe SORT]) -> [Named (FORMULA f)])
-> (Set PredType -> Map [SORT] (Set [Maybe SORT]))
-> Set PredType
-> [Named (FORMULA f)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SubSortMap -> Set PredType -> Map [SORT] (Set [Maybe SORT])
mkProfMapPred SubSortMap
subSortMap)
                   [] (Map SORT (Set PredType) -> [Named (FORMULA f)])
-> Map SORT (Set PredType) -> [Named (FORMULA f)]
forall a b. (a -> b) -> a -> b
$ PredMap -> Map SORT (Set PredType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap PredMap
pMap
          hi_axs :: [SenAttr (FORMULA f) String]
hi_axs =
          {- generate subclass_of axioms derived from subsorts
          and non-emptyness axioms -}
              (PredInfo -> [SenAttr (FORMULA f) String])
-> [PredInfo] -> [SenAttr (FORMULA f) String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ prdInf :: PredInfo
prdInf ->
               let ts :: SORT
ts = PredInfo -> SORT
topSortPI PredInfo
prdInf
                   subS :: SORT
subS = PredInfo -> SORT
predicatePI PredInfo
prdInf
                   set :: Set SORT
set = PredInfo -> Set SORT
directSuperSortsPI PredInfo
prdInf
                   supPreds :: [SORT]
supPreds = (SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (SubSortMap -> SORT -> SORT
lkupPred SubSortMap
subSortMap) ([SORT] -> [SORT]) -> [SORT] -> [SORT]
forall a b. (a -> b) -> a -> b
$ Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList Set SORT
set
                   x :: VAR_DECL
x = String -> SORT -> VAR_DECL
mkVarDeclStr "x" SORT
ts
                   mkPredf :: SORT -> FORMULA f
mkPredf sS :: SORT
sS = PRED_SYMB -> [TERM f] -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication (SORT -> SORT -> PRED_SYMB
mkSimpleQualPred SORT
sS SORT
ts)
                     [VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
x]
                in String -> FORMULA f -> SenAttr (FORMULA f) String
forall a s. a -> s -> SenAttr s a
makeNamed (SORT -> String
forall a. Show a => a -> String
show SORT
subS String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_non_empty")
                   (QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Existential [VAR_DECL
x] (SORT -> FORMULA f
forall f. SORT -> FORMULA f
mkPredf SORT
subS)
                     Range
nullRange)
                   SenAttr (FORMULA f) String
-> [SenAttr (FORMULA f) String] -> [SenAttr (FORMULA f) String]
forall a. a -> [a] -> [a]
: (SORT -> SenAttr (FORMULA f) String)
-> [SORT] -> [SenAttr (FORMULA f) String]
forall a b. (a -> b) -> [a] -> [b]
map (\ supS :: SORT
supS ->
                       String -> FORMULA f -> SenAttr (FORMULA f) String
forall a s. a -> s -> SenAttr s a
makeNamed (SORT -> String
forall a. Show a => a -> String
show SORT
subS String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_subclassOf_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show SORT
supS)
                       (FORMULA f -> SenAttr (FORMULA f) String)
-> FORMULA f -> SenAttr (FORMULA f) String
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL
x]
                          (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl (SORT -> FORMULA f
forall f. SORT -> FORMULA f
mkPredf SORT
subS) (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ SORT -> FORMULA f
forall f. SORT -> FORMULA f
mkPredf SORT
supS)
                         [SORT]
supPreds
             ) ([PredInfo] -> [SenAttr (FORMULA f) String])
-> [PredInfo] -> [SenAttr (FORMULA f) String]
forall a b. (a -> b) -> a -> b
$ SubSortMap -> [PredInfo]
forall k a. Map k a -> [a]
Map.elems SubSortMap
subSortMap

mkProfMapPred :: SubSortMap -> Set.Set PredType
              -> Map.Map [SORT] (Set.Set [Maybe PRED_NAME])
mkProfMapPred :: SubSortMap -> Set PredType -> Map [SORT] (Set [Maybe SORT])
mkProfMapPred ssm :: SubSortMap
ssm = (PredType
 -> Map [SORT] (Set [Maybe SORT]) -> Map [SORT] (Set [Maybe SORT]))
-> Map [SORT] (Set [Maybe SORT])
-> Set PredType
-> Map [SORT] (Set [Maybe SORT])
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold PredType
-> Map [SORT] (Set [Maybe SORT]) -> Map [SORT] (Set [Maybe SORT])
seperate Map [SORT] (Set [Maybe SORT])
forall k a. Map k a
Map.empty
    where seperate :: PredType
-> Map [SORT] (Set [Maybe SORT]) -> Map [SORT] (Set [Maybe SORT])
seperate pt :: PredType
pt = [SORT]
-> [Maybe SORT]
-> Map [SORT] (Set [Maybe SORT])
-> Map [SORT] (Set [Maybe SORT])
forall k a.
(Ord k, Ord a) =>
k -> a -> Map k (Set a) -> Map k (Set a)
MapSet.setInsert (PredType -> [SORT]
pt2topSorts PredType
pt) (PredType -> [Maybe SORT]
pt2preds PredType
pt)
          pt2topSorts :: PredType -> [SORT]
pt2topSorts = (SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (SubSortMap -> SORT -> SORT
lkupTop SubSortMap
ssm) ([SORT] -> [SORT]) -> (PredType -> [SORT]) -> PredType -> [SORT]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> [SORT]
predArgs
          pt2preds :: PredType -> [Maybe SORT]
pt2preds = (SORT -> Maybe SORT) -> [SORT] -> [Maybe SORT]
forall a b. (a -> b) -> [a] -> [b]
map (SubSortMap -> SORT -> Maybe SORT
lkupPredM SubSortMap
ssm) ([SORT] -> [Maybe SORT])
-> (PredType -> [SORT]) -> PredType -> [Maybe SORT]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> [SORT]
predArgs

mkProfMapOp :: SubSortMap -> Set.Set OpType
            -> Map.Map [SORT] (OpKind, Set.Set [Maybe PRED_NAME])
mkProfMapOp :: SubSortMap -> Set OpType -> Map [SORT] (OpKind, Set [Maybe SORT])
mkProfMapOp ssm :: SubSortMap
ssm = (OpType
 -> Map [SORT] (OpKind, Set [Maybe SORT])
 -> Map [SORT] (OpKind, Set [Maybe SORT]))
-> Map [SORT] (OpKind, Set [Maybe SORT])
-> Set OpType
-> Map [SORT] (OpKind, Set [Maybe SORT])
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold OpType
-> Map [SORT] (OpKind, Set [Maybe SORT])
-> Map [SORT] (OpKind, Set [Maybe SORT])
seperate Map [SORT] (OpKind, Set [Maybe SORT])
forall k a. Map k a
Map.empty
    where seperate :: OpType
-> Map [SORT] (OpKind, Set [Maybe SORT])
-> Map [SORT] (OpKind, Set [Maybe SORT])
seperate ot :: OpType
ot =
              ((OpKind, Set [Maybe SORT])
 -> (OpKind, Set [Maybe SORT]) -> (OpKind, Set [Maybe SORT]))
-> [SORT]
-> (OpKind, Set [Maybe SORT])
-> Map [SORT] (OpKind, Set [Maybe SORT])
-> Map [SORT] (OpKind, Set [Maybe SORT])
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (\ (k1 :: OpKind
k1, s1 :: Set [Maybe SORT]
s1) (k2 :: OpKind
k2, s2 :: Set [Maybe SORT]
s2) ->
                                           (OpKind -> OpKind -> OpKind
forall a. Ord a => a -> a -> a
min OpKind
k1 OpKind
k2, Set [Maybe SORT] -> Set [Maybe SORT] -> Set [Maybe SORT]
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set [Maybe SORT]
s1 Set [Maybe SORT]
s2))
                ([SORT] -> [SORT]
pt2topSorts [SORT]
joinedList)
                (OpKind
fKind, [Maybe SORT] -> Set [Maybe SORT]
forall a. a -> Set a
Set.singleton ([Maybe SORT] -> Set [Maybe SORT])
-> [Maybe SORT] -> Set [Maybe SORT]
forall a b. (a -> b) -> a -> b
$ [SORT] -> [Maybe SORT]
pt2preds [SORT]
joinedList)
              where joinedList :: [SORT]
joinedList = OpType -> [SORT]
opSorts OpType
ot
                    fKind :: OpKind
fKind = OpType -> OpKind
opKind OpType
ot
                    pt2topSorts :: [SORT] -> [SORT]
pt2topSorts = (SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (SubSortMap -> SORT -> SORT
lkupTop SubSortMap
ssm)
                    pt2preds :: [SORT] -> [Maybe SORT]
pt2preds = (SORT -> Maybe SORT) -> [SORT] -> [Maybe SORT]
forall a b. (a -> b) -> [a] -> [b]
map (SubSortMap -> SORT -> Maybe SORT
lkupPredM SubSortMap
ssm)

lkupTop :: SubSortMap -> SORT -> SORT
lkupTop :: SubSortMap -> SORT -> SORT
lkupTop ssm :: SubSortMap
ssm s :: SORT
s = SORT -> (PredInfo -> SORT) -> Maybe PredInfo -> SORT
forall b a. b -> (a -> b) -> Maybe a -> b
maybe SORT
s PredInfo -> SORT
topSortPI (SORT -> SubSortMap -> Maybe PredInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SORT
s SubSortMap
ssm)

lkupPredM :: SubSortMap -> SORT -> Maybe PRED_NAME
lkupPredM :: SubSortMap -> SORT -> Maybe SORT
lkupPredM ssm :: SubSortMap
ssm s :: SORT
s = (PredInfo -> SORT) -> Maybe PredInfo -> Maybe SORT
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PredInfo -> SORT
predicatePI (Maybe PredInfo -> Maybe SORT) -> Maybe PredInfo -> Maybe SORT
forall a b. (a -> b) -> a -> b
$ SORT -> SubSortMap -> Maybe PredInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SORT
s SubSortMap
ssm

lkupPred :: SubSortMap -> SORT -> PRED_NAME
lkupPred :: SubSortMap -> SORT -> SORT
lkupPred ssm :: SubSortMap
ssm = SORT -> Maybe SORT -> SORT
forall a. a -> Maybe a -> a
fromMaybe (String -> SORT
forall a. HasCallStack => String -> a
error "CASL2TopSort.lkupPred") (Maybe SORT -> SORT) -> (SORT -> Maybe SORT) -> SORT -> SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SubSortMap -> SORT -> Maybe SORT
lkupPredM SubSortMap
ssm

genArgRest :: String -> ([VAR_DECL] -> FORMULA f)
               {- ^ generates from a list of variables
               either the predication or function equation -}
           -> [SORT] -> Set.Set [Maybe PRED_NAME]
           -> [Named (FORMULA f)] -> [Named (FORMULA f)]
genArgRest :: String
-> ([VAR_DECL] -> FORMULA f)
-> [SORT]
-> Set [Maybe SORT]
-> [Named (FORMULA f)]
-> [Named (FORMULA f)]
genArgRest sen_name :: String
sen_name genProp :: [VAR_DECL] -> FORMULA f
genProp sl :: [SORT]
sl spl :: Set [Maybe SORT]
spl fs :: [Named (FORMULA f)]
fs =
    let vars :: [VAR_DECL]
vars = [SORT] -> [VAR_DECL]
genVars [SORT]
sl
        mquant :: Maybe (FORMULA f)
mquant = FORMULA f -> [VAR_DECL] -> Set [Maybe SORT] -> Maybe (FORMULA f)
forall f.
FORMULA f -> [VAR_DECL] -> Set [Maybe SORT] -> Maybe (FORMULA f)
genQuantification ([VAR_DECL] -> FORMULA f
genProp [VAR_DECL]
vars) [VAR_DECL]
vars Set [Maybe SORT]
spl
    in [Named (FORMULA f)]
-> (FORMULA f -> [Named (FORMULA f)])
-> Maybe (FORMULA f)
-> [Named (FORMULA f)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Named (FORMULA f)]
fs (\ quant :: FORMULA f
quant -> String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed String
sen_name FORMULA f
quant Named (FORMULA f) -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. a -> [a] -> [a]
: [Named (FORMULA f)]
fs) Maybe (FORMULA f)
mquant

genPredication :: PRED_NAME -> [VAR_DECL] -> FORMULA f
genPredication :: SORT -> [VAR_DECL] -> FORMULA f
genPredication pName :: SORT
pName vars :: [VAR_DECL]
vars =
  SORT -> [SORT] -> [TERM f] -> FORMULA f
forall f. SORT -> [SORT] -> [TERM f] -> FORMULA f
genPredAppl SORT
pName ((VAR_DECL -> SORT) -> [VAR_DECL] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Var_decl _ s :: SORT
s _) -> SORT
s) [VAR_DECL]
vars) ([TERM f] -> FORMULA f) -> [TERM f] -> FORMULA f
forall a b. (a -> b) -> a -> b
$ (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]
vars

-- | generate a predication with qualified pred name
genPredAppl :: PRED_NAME -> [SORT] -> [TERM f] -> FORMULA f
genPredAppl :: SORT -> [SORT] -> [TERM f] -> FORMULA f
genPredAppl pName :: SORT
pName sl :: [SORT]
sl terms :: [TERM f]
terms = PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (SORT -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name SORT
pName
    ([SORT] -> Range -> PRED_TYPE
Pred_type [SORT]
sl Range
nullRange) Range
nullRange) [TERM f]
terms Range
nullRange

genOpEquation :: OpKind -> OP_NAME -> [VAR_DECL] -> FORMULA f
genOpEquation :: OpKind -> SORT -> [VAR_DECL] -> FORMULA f
genOpEquation kind :: OpKind
kind opName :: SORT
opName vars :: [VAR_DECL]
vars = case [VAR_DECL]
vars of
  resV :: VAR_DECL
resV@(Var_decl _ s :: SORT
s _) : argVs :: [VAR_DECL]
argVs -> TERM f -> TERM f -> FORMULA f
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM f
forall f. TERM f
opTerm TERM f
forall f. TERM f
resTerm
    where opTerm :: TERM f
opTerm = OP_SYMB -> [TERM f] -> TERM f
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl (SORT -> OP_TYPE -> OP_SYMB
mkQualOp SORT
opName OP_TYPE
opType) [TERM f]
forall f. [TERM f]
argTerms
          opType :: OP_TYPE
opType = OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
kind [SORT]
argSorts SORT
s Range
nullRange
          argSorts :: [SORT]
argSorts = [VAR_DECL] -> [SORT]
sortsOfArgs [VAR_DECL]
argVs
          resTerm :: TERM f
resTerm = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
resV
          argTerms :: [TERM f]
argTerms = (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]
argVs
  _ -> String -> FORMULA f
forall a. HasCallStack => String -> a
error "CASL2TopSort.genOpEquation: no result variable"

genVars :: [SORT] -> [VAR_DECL]
genVars :: [SORT] -> [VAR_DECL]
genVars = (String -> SORT -> VAR_DECL) -> [String] -> [SORT] -> [VAR_DECL]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith String -> SORT -> VAR_DECL
mkVarDeclStr [String]
varSymbs
    where varSymbs :: [String]
varSymbs =
            (Char -> String) -> String -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Char -> ShowS
forall a. a -> [a] -> [a]
: []) "xyzuwv" [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ i :: Int
i -> 'v' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
i) [(1 :: Int) ..]

genSenName :: Show a => String -> a -> Int -> String
genSenName :: String -> a -> Int -> String
genSenName suff :: String
suff symbName :: a
symbName arity :: Int
arity =
    "arg_rest_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
symbName String -> ShowS
forall a. [a] -> [a] -> [a]
++ '_' Char -> ShowS
forall a. a -> [a] -> [a]
: String
suff String -> ShowS
forall a. [a] -> [a] -> [a]
++ '_' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
arity

genQuantification :: FORMULA f {- ^ either the predication or
                               function equation -}
                  -> [VAR_DECL] -- ^ Qual_vars
                  -> Set.Set [Maybe PRED_NAME]
                  -> Maybe (FORMULA f)
genQuantification :: FORMULA f -> [VAR_DECL] -> Set [Maybe SORT] -> Maybe (FORMULA f)
genQuantification prop :: FORMULA f
prop vars :: [VAR_DECL]
vars spl :: Set [Maybe SORT]
spl = do
     FORMULA f
dis <- [VAR_DECL] -> Set [Maybe SORT] -> Maybe (FORMULA f)
forall f. [VAR_DECL] -> Set [Maybe SORT] -> Maybe (FORMULA f)
genDisjunction [VAR_DECL]
vars Set [Maybe SORT]
spl
     FORMULA f -> Maybe (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> Maybe (FORMULA f)) -> FORMULA f -> Maybe (FORMULA f)
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL]
vars (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl FORMULA f
prop FORMULA f
dis

genDisjunction :: [VAR_DECL] -> Set.Set [Maybe PRED_NAME] -> Maybe (FORMULA f)
genDisjunction :: [VAR_DECL] -> Set [Maybe SORT] -> Maybe (FORMULA f)
genDisjunction vars :: [VAR_DECL]
vars spn :: Set [Maybe SORT]
spn
    | Set [Maybe SORT] -> Int
forall a. Set a -> Int
Set.size Set [Maybe SORT]
spn Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 =
        case [FORMULA f]
forall f. [FORMULA f]
disjs of
        [] -> Maybe (FORMULA f)
forall a. Maybe a
Nothing
        [x :: FORMULA f
x] -> FORMULA f -> Maybe (FORMULA f)
forall a. a -> Maybe a
Just FORMULA f
x
        _ -> String -> Maybe (FORMULA f)
forall a. HasCallStack => String -> a
error "CASL2TopSort.genDisjunction: this cannot happen"
    | [FORMULA Any] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FORMULA Any]
forall f. [FORMULA f]
disjs = Maybe (FORMULA f)
forall a. Maybe a
Nothing
    | Bool
otherwise = FORMULA f -> Maybe (FORMULA f)
forall a. a -> Maybe a
Just ([FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
disjunct [FORMULA f]
forall f. [FORMULA f]
disjs)
      where disjs :: [FORMULA f]
disjs = ([FORMULA f] -> [Maybe SORT] -> [FORMULA f])
-> [FORMULA f] -> [[Maybe SORT]] -> [FORMULA f]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl [FORMULA f] -> [Maybe SORT] -> [FORMULA f]
forall f. [FORMULA f] -> [Maybe SORT] -> [FORMULA f]
genConjunction [] (Set [Maybe SORT] -> [[Maybe SORT]]
forall a. Set a -> [a]
Set.toList Set [Maybe SORT]
spn)
            genConjunction :: [FORMULA f] -> [Maybe SORT] -> [FORMULA f]
genConjunction acc :: [FORMULA f]
acc pns :: [Maybe SORT]
pns
                | [FORMULA Any] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FORMULA Any]
forall f. [FORMULA f]
conjs = [FORMULA f]
acc
                | Bool
otherwise = [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct ([FORMULA f] -> [FORMULA f]
forall a. [a] -> [a]
reverse [FORMULA f]
forall f. [FORMULA f]
conjs) FORMULA f -> [FORMULA f] -> [FORMULA f]
forall a. a -> [a] -> [a]
: [FORMULA f]
acc
                where conjs :: [FORMULA f]
conjs = ([FORMULA f] -> (VAR_DECL, Maybe SORT) -> [FORMULA f])
-> [FORMULA f] -> [(VAR_DECL, Maybe SORT)] -> [FORMULA f]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl [FORMULA f] -> (VAR_DECL, Maybe SORT) -> [FORMULA f]
forall f. [FORMULA f] -> (VAR_DECL, Maybe SORT) -> [FORMULA f]
genPred [] ([VAR_DECL] -> [Maybe SORT] -> [(VAR_DECL, Maybe SORT)]
forall a b. [a] -> [b] -> [(a, b)]
zip [VAR_DECL]
vars [Maybe SORT]
pns)
            genPred :: [FORMULA f] -> (VAR_DECL, Maybe SORT) -> [FORMULA f]
genPred acc :: [FORMULA f]
acc (v :: VAR_DECL
v, mpn :: Maybe SORT
mpn) = [FORMULA f] -> (SORT -> [FORMULA f]) -> Maybe SORT -> [FORMULA f]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [FORMULA f]
acc
                (\ pn :: SORT
pn -> SORT -> [VAR_DECL] -> FORMULA f
forall f. SORT -> [VAR_DECL] -> FORMULA f
genPredication SORT
pn [VAR_DECL
v] FORMULA f -> [FORMULA f] -> [FORMULA f]
forall a. a -> [a] -> [a]
: [FORMULA f]
acc) Maybe SORT
mpn

{- | Each membership test of a subsort is transformed to a predication
of the corresponding unary predicate. Variables quantified over a
subsort yield a premise to the quantified formula that the
corresponding predicate holds. All typings are adjusted according
to the subsortmap and sort generation constraints are translated to
disjointness axioms. -}

transSen :: Sign f e -> FORMULA f -> Result (FORMULA f)
transSen :: Sign f e -> FORMULA f -> Result (FORMULA f)
transSen sig :: Sign f e
sig f :: FORMULA f
f = let sortRels :: Rel SORT
sortRels = Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.rmNullSets (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
sig in
    if Rel SORT -> Bool
forall a. Ord a => Rel a -> Bool
Rel.noPairs Rel SORT
sortRels then FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return FORMULA f
f else do
    let ssm :: SubSortMap
ssm = Rel SORT -> PredMap -> SubSortMap
generateSubSortMap Rel SORT
sortRels (Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
sig)
        newOpMap :: OpMap
newOpMap = Rel SORT -> SubSortMap -> OpMap -> OpMap
transOpMap Rel SORT
sortRels SubSortMap
ssm (Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
sig)
    SubSortMap -> OpMap -> FORMULA f -> Result (FORMULA f)
forall f. SubSortMap -> OpMap -> FORMULA f -> Result (FORMULA f)
mapSen SubSortMap
ssm OpMap
newOpMap FORMULA f
f

mapSen :: SubSortMap -> OpMap -> FORMULA f -> Result (FORMULA f)
mapSen :: SubSortMap -> OpMap -> FORMULA f -> Result (FORMULA f)
mapSen ssMap :: SubSortMap
ssMap opM :: OpMap
opM f :: FORMULA f
f =
    case FORMULA f
f of
    Sort_gen_ax cs :: [Constraint]
cs _ ->
        SubSortMap -> [Constraint] -> Result (FORMULA f)
forall f. SubSortMap -> [Constraint] -> Result (FORMULA f)
genEitherAxiom SubSortMap
ssMap [Constraint]
cs
    _ -> FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> Result (FORMULA f))
-> FORMULA f -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (SubSortMap -> OpMap -> Record f (FORMULA f) (TERM f)
forall f. SubSortMap -> OpMap -> Record f (FORMULA f) (TERM f)
mapRec SubSortMap
ssMap OpMap
opM) FORMULA f
f

mapRec :: SubSortMap -> OpMap -> Record f (FORMULA f) (TERM f)
mapRec :: SubSortMap -> OpMap -> Record f (FORMULA f) (TERM f)
mapRec ssM :: SubSortMap
ssM opM :: OpMap
opM = ((f -> f) -> Record f (FORMULA f) (TERM f)
forall f g. (f -> g) -> Record f (FORMULA g) (TERM g)
mapRecord f -> f
forall a. a -> a
id)
  { foldQuantification :: FORMULA f
-> QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
foldQuantification = \ _ q :: QUANTIFIER
q vdl :: [VAR_DECL]
vdl ->
        QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q ((VAR_DECL -> VAR_DECL) -> [VAR_DECL] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map VAR_DECL -> VAR_DECL
updateVarDecls [VAR_DECL]
vdl) (FORMULA f -> Range -> FORMULA f)
-> (FORMULA f -> FORMULA f) -> FORMULA f -> Range -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QUANTIFIER -> [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. QUANTIFIER -> [VAR_DECL] -> FORMULA f -> FORMULA f
relativize QUANTIFIER
q [VAR_DECL]
vdl
  , foldMembership :: FORMULA f -> TERM f -> SORT -> Range -> FORMULA f
foldMembership = \ _ t :: TERM f
t s :: SORT
s pl :: Range
pl -> FORMULA f -> (SORT -> FORMULA f) -> Maybe SORT -> FORMULA f
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (TERM f -> SORT -> Range -> FORMULA f
forall f. TERM f -> SORT -> Range -> FORMULA f
Membership TERM f
t SORT
s Range
pl)
      (\ pn :: SORT
pn -> SORT -> [SORT] -> [TERM f] -> FORMULA f
forall f. SORT -> [SORT] -> [TERM f] -> FORMULA f
genPredAppl SORT
pn [SORT -> SORT
lTop SORT
s] [TERM f
t]) (Maybe SORT -> FORMULA f) -> Maybe SORT -> FORMULA f
forall a b. (a -> b) -> a -> b
$ SORT -> Maybe SORT
lPred SORT
s
  , foldPredication :: FORMULA f -> PRED_SYMB -> [TERM f] -> Range -> FORMULA f
foldPredication = \ _ -> PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (PRED_SYMB -> [TERM f] -> Range -> FORMULA f)
-> (PRED_SYMB -> PRED_SYMB)
-> PRED_SYMB
-> [TERM f]
-> Range
-> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PRED_SYMB -> PRED_SYMB
updatePRED_SYMB
  , foldQual_var :: TERM f -> VAR -> SORT -> Range -> TERM f
foldQual_var = \ _ v :: VAR
v -> VAR -> SORT -> Range -> TERM f
forall f. VAR -> SORT -> Range -> TERM f
Qual_var VAR
v (SORT -> Range -> TERM f)
-> (SORT -> SORT) -> SORT -> Range -> TERM f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> SORT
lTop
  , foldApplication :: TERM f -> OP_SYMB -> [TERM f] -> Range -> TERM f
foldApplication = \ _ -> OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (OP_SYMB -> [TERM f] -> Range -> TERM f)
-> (OP_SYMB -> OP_SYMB) -> OP_SYMB -> [TERM f] -> Range -> TERM f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OP_SYMB -> OP_SYMB
updateOP_SYMB
  , foldSorted_term :: TERM f -> TERM f -> SORT -> Range -> TERM f
foldSorted_term = \ _ t1 :: TERM f
t1 -> TERM f -> SORT -> Range -> TERM f
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term TERM f
t1 (SORT -> Range -> TERM f)
-> (SORT -> SORT) -> SORT -> Range -> TERM f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> SORT
lTop
    -- casts are discarded due to missing subsorting
  , foldCast :: TERM f -> TERM f -> SORT -> Range -> TERM f
foldCast = \ _ t1 :: TERM f
t1 _ _ -> TERM f
t1 }
    where lTop :: SORT -> SORT
lTop = SubSortMap -> SORT -> SORT
lkupTop SubSortMap
ssM
          lPred :: SORT -> Maybe SORT
lPred = SubSortMap -> SORT -> Maybe SORT
lkupPredM SubSortMap
ssM
          updateOP_SYMB :: OP_SYMB -> OP_SYMB
updateOP_SYMB (Op_name _) =
              String -> OP_SYMB
forall a. HasCallStack => String -> a
error "CASL2TopSort.mapTerm: got untyped application"
          updateOP_SYMB (Qual_op_name on :: SORT
on ot :: OP_TYPE
ot pl :: Range
pl) =
              SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
on (SORT -> OP_TYPE -> OP_TYPE
updateOP_TYPE SORT
on OP_TYPE
ot) Range
pl
          updateOP_TYPE :: SORT -> OP_TYPE -> OP_TYPE
updateOP_TYPE on :: SORT
on (Op_type _ sl :: [SORT]
sl s :: SORT
s pl :: Range
pl) =
              let args :: [SORT]
args = (SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> SORT
lTop [SORT]
sl
                  res :: SORT
res = SORT -> SORT
lTop SORT
s
                  t1 :: OpType
t1 = OP_TYPE -> OpType
toOpType (OP_TYPE -> OpType) -> OP_TYPE -> OpType
forall a b. (a -> b) -> a -> b
$ OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [SORT]
args SORT
res Range
pl
                  ts :: Set OpType
ts = SORT -> OpMap -> Set OpType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup SORT
on OpMap
opM
                  nK :: OpKind
nK = if OpType -> Set OpType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member OpType
t1 Set OpType
ts then OpKind
Total else OpKind
Partial
              in OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
nK [SORT]
args SORT
res Range
pl
          updateVarDecls :: VAR_DECL -> VAR_DECL
updateVarDecls (Var_decl vl :: [VAR]
vl s :: SORT
s pl :: Range
pl) =
              [VAR] -> SORT -> Range -> VAR_DECL
Var_decl [VAR]
vl (SORT -> SORT
lTop SORT
s) Range
pl
          updatePRED_SYMB :: PRED_SYMB -> PRED_SYMB
updatePRED_SYMB (Pred_name _) =
              String -> PRED_SYMB
forall a. HasCallStack => String -> a
error "CASL2TopSort.mapSen: got untyped predication"
          updatePRED_SYMB (Qual_pred_name pn :: SORT
pn (Pred_type sl :: [SORT]
sl pl' :: Range
pl') pl :: Range
pl) =
              SORT -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name SORT
pn
                 ([SORT] -> Range -> PRED_TYPE
Pred_type ((SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> SORT
lTop [SORT]
sl) Range
pl') Range
pl
          -- relativize quantifiers using predicates coding sorts
          relativize :: QUANTIFIER -> [VAR_DECL] -> FORMULA f -> FORMULA f
relativize q :: QUANTIFIER
q vdl :: [VAR_DECL]
vdl f1 :: FORMULA f
f1 = let vPs :: FORMULA f
vPs = [VAR_DECL] -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f
mkVarPreds [VAR_DECL]
vdl in
              if [VAR_DECL] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VAR_DECL]
vdl then FORMULA f
f1
              else case QUANTIFIER
q of  -- universal? then use implication
                Universal -> FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl FORMULA f
forall f. FORMULA f
vPs FORMULA f
f1
                -- existential or unique-existential? then use conjuction
                _ -> [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct [FORMULA f
forall f. FORMULA f
vPs, FORMULA f
f1]
          mkVarPreds :: [VAR_DECL] -> FORMULA f
mkVarPreds = [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct ([FORMULA f] -> FORMULA f)
-> ([VAR_DECL] -> [FORMULA f]) -> [VAR_DECL] -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VAR_DECL -> FORMULA f) -> [VAR_DECL] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map VAR_DECL -> FORMULA f
forall f. VAR_DECL -> FORMULA f
mkVarPred
          mkVarPred :: VAR_DECL -> FORMULA f
mkVarPred (Var_decl vs :: [VAR]
vs s :: SORT
s _) = [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct ([FORMULA f] -> FORMULA f) -> [FORMULA f] -> FORMULA f
forall a b. (a -> b) -> a -> b
$ (VAR -> [FORMULA f] -> [FORMULA f])
-> [FORMULA f] -> [VAR] -> [FORMULA f]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (SORT -> VAR -> [FORMULA f] -> [FORMULA f]
forall f. SORT -> VAR -> [FORMULA f] -> [FORMULA f]
mkVarPred1 SORT
s) [] [VAR]
vs
          mkVarPred1 :: SORT -> VAR -> [FORMULA f] -> [FORMULA f]
mkVarPred1 s :: SORT
s v :: VAR
v = case SORT -> Maybe SORT
lPred SORT
s of
                 -- no subsort? then no relativization
                 Nothing -> [FORMULA f] -> [FORMULA f]
forall a. a -> a
id
                 Just p1 :: SORT
p1 -> (SORT -> [VAR_DECL] -> FORMULA f
forall f. SORT -> [VAR_DECL] -> FORMULA f
genPredication SORT
p1 [VAR -> SORT -> VAR_DECL
mkVarDecl VAR
v (SORT -> VAR_DECL) -> SORT -> VAR_DECL
forall a b. (a -> b) -> a -> b
$ SORT -> SORT
lTop SORT
s] FORMULA f -> [FORMULA f] -> [FORMULA f]
forall a. a -> [a] -> [a]
:)

genEitherAxiom :: SubSortMap -> [Constraint] -> Result (FORMULA f)
genEitherAxiom :: SubSortMap -> [Constraint] -> Result (FORMULA f)
genEitherAxiom ssMap :: SubSortMap
ssMap =
    [OP_SYMB] -> Result (FORMULA f)
forall f. [OP_SYMB] -> Result (FORMULA f)
genConjunction ([OP_SYMB] -> Result (FORMULA f))
-> ([Constraint] -> [OP_SYMB])
-> [Constraint]
-> Result (FORMULA f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\ (_, osl :: [OP_SYMB]
osl, _) -> [OP_SYMB]
osl) (([SORT], [OP_SYMB], [(SORT, SORT)]) -> [OP_SYMB])
-> ([Constraint] -> ([SORT], [OP_SYMB], [(SORT, SORT)]))
-> [Constraint]
-> [OP_SYMB]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Constraint] -> ([SORT], [OP_SYMB], [(SORT, SORT)])
recover_Sort_gen_ax
    where genConjunction :: [OP_SYMB] -> Result (FORMULA f)
genConjunction osl :: [OP_SYMB]
osl =
            let (injOps :: [OP_SYMB]
injOps, constrs :: [OP_SYMB]
constrs) = (OP_SYMB -> Bool) -> [OP_SYMB] -> ([OP_SYMB], [OP_SYMB])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition OP_SYMB -> Bool
isInjOp [OP_SYMB]
osl
                groupedInjOps :: [[OP_SYMB]]
groupedInjOps = (OP_SYMB -> OP_SYMB -> Bool) -> [OP_SYMB] -> [[OP_SYMB]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy OP_SYMB -> OP_SYMB -> Bool
sameTarget ([OP_SYMB] -> [[OP_SYMB]]) -> [OP_SYMB] -> [[OP_SYMB]]
forall a b. (a -> b) -> a -> b
$ (OP_SYMB -> OP_SYMB -> Ordering) -> [OP_SYMB] -> [OP_SYMB]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy OP_SYMB -> OP_SYMB -> Ordering
compTarget [OP_SYMB]
injOps
            in if [OP_SYMB] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [OP_SYMB]
constrs
               then case [[OP_SYMB]]
groupedInjOps of
                    [] -> String -> Range -> Result (FORMULA f)
forall a. String -> Range -> Result a
fatal_error "No injective operation found" Range
nullRange
                    [xs :: [OP_SYMB]
xs@(x :: OP_SYMB
x : _)] -> FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> Result (FORMULA f))
-> FORMULA f -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ OP_SYMB -> FORMULA f -> FORMULA f
forall f. OP_SYMB -> FORMULA f -> FORMULA f
genQuant OP_SYMB
x (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ [OP_SYMB] -> FORMULA f
forall f. [OP_SYMB] -> FORMULA f
genImpl [OP_SYMB]
xs
                    ((x :: OP_SYMB
x : _) : _) -> FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> Result (FORMULA f))
-> FORMULA f -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ OP_SYMB -> FORMULA f -> FORMULA f
forall f. OP_SYMB -> FORMULA f -> FORMULA f
genQuant OP_SYMB
x
                        (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct ([FORMULA f] -> FORMULA f) -> [FORMULA f] -> FORMULA f
forall a b. (a -> b) -> a -> b
$ ([OP_SYMB] -> FORMULA f) -> [[OP_SYMB]] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map [OP_SYMB] -> FORMULA f
forall f. [OP_SYMB] -> FORMULA f
genImpl [[OP_SYMB]]
groupedInjOps
                    _ -> String -> Result (FORMULA f)
forall a. HasCallStack => String -> a
error "CASL2TopSort.genEitherAxiom.groupedInjOps"
               else [Diagnosis] -> Maybe (FORMULA f) -> Result (FORMULA f)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> [OP_SYMB] -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint
                            "ignoring generating constructors"
                            [OP_SYMB]
constrs]
                    (Maybe (FORMULA f) -> Result (FORMULA f))
-> Maybe (FORMULA f) -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ FORMULA f -> Maybe (FORMULA f)
forall a. a -> Maybe a
Just FORMULA f
forall f. FORMULA f
trueForm
          isInjOp :: OP_SYMB -> Bool
isInjOp ops :: OP_SYMB
ops =
              case OP_SYMB
ops of
              Op_name _ -> String -> Bool
forall a. HasCallStack => String -> a
error "CASL2TopSort.genEitherAxiom.isInjObj"
              Qual_op_name on :: SORT
on _ _ -> SORT -> Bool
isInjName SORT
on
          resultSort :: OP_SYMB -> SORT
resultSort (Qual_op_name _ (Op_type _ _ t :: SORT
t _) _) = SORT
t
          resultSort _ = String -> SORT
forall a. HasCallStack => String -> a
error "CASL2TopSort.genEitherAxiom.resultSort"
          argSort :: OP_SYMB -> SORT
argSort (Qual_op_name _ (Op_type _ [x :: SORT
x] _ _) _) = SORT
x
          argSort _ = String -> SORT
forall a. HasCallStack => String -> a
error "CASL2TopSort.genEitherAxiom.argSort"
          compTarget :: OP_SYMB -> OP_SYMB -> Ordering
compTarget = (OP_SYMB -> SORT) -> OP_SYMB -> OP_SYMB -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing OP_SYMB -> SORT
resultSort
          sameTarget :: OP_SYMB -> OP_SYMB -> Bool
sameTarget x1 :: OP_SYMB
x1 x2 :: OP_SYMB
x2 = OP_SYMB -> OP_SYMB -> Ordering
compTarget OP_SYMB
x1 OP_SYMB
x2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ
          lTop :: SORT -> SORT
lTop = SubSortMap -> SORT -> SORT
lkupTop SubSortMap
ssMap
          mkXVarDecl :: OP_SYMB -> VAR_DECL
mkXVarDecl = String -> SORT -> VAR_DECL
mkVarDeclStr "x" (SORT -> VAR_DECL) -> (OP_SYMB -> SORT) -> OP_SYMB -> VAR_DECL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> SORT
lTop (SORT -> SORT) -> (OP_SYMB -> SORT) -> OP_SYMB -> SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OP_SYMB -> SORT
resultSort
          genQuant :: OP_SYMB -> FORMULA f -> FORMULA f
genQuant qon :: OP_SYMB
qon = [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [OP_SYMB -> VAR_DECL
mkXVarDecl OP_SYMB
qon]
          genImpl :: [OP_SYMB] -> FORMULA f
genImpl xs :: [OP_SYMB]
xs = case [OP_SYMB]
xs of
            x :: OP_SYMB
x : _ -> let
              rSrt :: SORT
rSrt = OP_SYMB -> SORT
resultSort OP_SYMB
x
              ltSrt :: SORT
ltSrt = SORT -> SORT
lTop SORT
rSrt
              disjs :: FORMULA f
disjs = [OP_SYMB] -> FORMULA f
forall f. [OP_SYMB] -> FORMULA f
genDisj [OP_SYMB]
xs
              in if SORT
ltSrt SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT -> SORT
lTop (OP_SYMB -> SORT
argSort OP_SYMB
x) then
                   if SORT
rSrt SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
ltSrt then FORMULA f
forall f. FORMULA f
disjs else FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl (OP_SYMB -> FORMULA f
forall f. OP_SYMB -> FORMULA f
genProp OP_SYMB
x) FORMULA f
forall f. FORMULA f
disjs
                 else String -> FORMULA f
forall a. HasCallStack => String -> a
error "CASL2TopSort.genEitherAxiom.genImpl"
            _ -> String -> FORMULA f
forall a. HasCallStack => String -> a
error "CASL2TopSort.genEitherAxiom.genImpl No OP_SYMB found"
          genProp :: OP_SYMB -> FORMULA f
genProp qon :: OP_SYMB
qon =
              SORT -> [VAR_DECL] -> FORMULA f
forall f. SORT -> [VAR_DECL] -> FORMULA f
genPredication (SORT -> SORT
lPredName (SORT -> SORT) -> SORT -> SORT
forall a b. (a -> b) -> a -> b
$ OP_SYMB -> SORT
resultSort OP_SYMB
qon) [OP_SYMB -> VAR_DECL
mkXVarDecl OP_SYMB
qon]
          lPredName :: SORT -> SORT
lPredName = SubSortMap -> SORT -> SORT
lkupPred SubSortMap
ssMap
          genDisj :: [OP_SYMB] -> FORMULA f
genDisj qons :: [OP_SYMB]
qons = [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
disjunct ((OP_SYMB -> FORMULA f) -> [OP_SYMB] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map OP_SYMB -> FORMULA f
forall f. OP_SYMB -> FORMULA f
genPred [OP_SYMB]
qons)
          genPred :: OP_SYMB -> FORMULA f
genPred qon :: OP_SYMB
qon =
              SORT -> [VAR_DECL] -> FORMULA f
forall f. SORT -> [VAR_DECL] -> FORMULA f
genPredication (SORT -> SORT
lPredName (SORT -> SORT) -> SORT -> SORT
forall a b. (a -> b) -> a -> b
$ OP_SYMB -> SORT
argSort OP_SYMB
qon) [OP_SYMB -> VAR_DECL
mkXVarDecl OP_SYMB
qon]