{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/SuleCFOL2SoftFOL.hs
Description :  Coding of a CASL subset into SoftFOL
Copyright   :  (c) Klaus Luettich and Uni Bremen 2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

The translating comorphism from a CASL subset to SoftFOL.
-}

module Comorphisms.SuleCFOL2SoftFOL
  ( suleCFOL2SoftFOL
  , suleCFOL2SoftFOLInduction
  , suleCFOL2SoftFOLInduction2
  , extractCASLModel
  ) where

import Control.Exception (assert)
import Control.Monad (foldM)
import qualified Control.Monad.Fail as Fail

import Logic.Logic as Logic
import Logic.Comorphism

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

import Text.ParserCombinators.Parsec
import qualified Data.Map as Map
import qualified Data.Set as Set

import Data.List as List
import Data.Maybe
import Data.Char
import Data.Function

import CASL.Logic_CASL
import CASL.AS_Basic_CASL
import CASL.Cycle
import CASL.Sublogic as SL
import CASL.Sign as CSign
import CASL.MapSentence
import CASL.Morphism
import CASL.Quantification
import CASL.Overload
import CASL.Utils
import CASL.Inject
import CASL.Induction (generateInductionLemmas)
import CASL.Simplify
import CASL.ToDoc

import SoftFOL.Sign as SPSign
import SoftFOL.Logic_SoftFOL
import SoftFOL.Translate
import SoftFOL.ParseTPTP

data PlainSoftFOL = PlainSoftFOL

instance Show PlainSoftFOL where
  show :: PlainSoftFOL -> String
show PlainSoftFOL = "SoftFOL"

data SoftFOLInduction = SoftFOLInduction deriving Int -> SoftFOLInduction -> ShowS
[SoftFOLInduction] -> ShowS
SoftFOLInduction -> String
(Int -> SoftFOLInduction -> ShowS)
-> (SoftFOLInduction -> String)
-> ([SoftFOLInduction] -> ShowS)
-> Show SoftFOLInduction
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SoftFOLInduction] -> ShowS
$cshowList :: [SoftFOLInduction] -> ShowS
show :: SoftFOLInduction -> String
$cshow :: SoftFOLInduction -> String
showsPrec :: Int -> SoftFOLInduction -> ShowS
$cshowsPrec :: Int -> SoftFOLInduction -> ShowS
Show
data SoftFOLInduction2 = SoftFOLInduction2 deriving Int -> SoftFOLInduction2 -> ShowS
[SoftFOLInduction2] -> ShowS
SoftFOLInduction2 -> String
(Int -> SoftFOLInduction2 -> ShowS)
-> (SoftFOLInduction2 -> String)
-> ([SoftFOLInduction2] -> ShowS)
-> Show SoftFOLInduction2
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SoftFOLInduction2] -> ShowS
$cshowList :: [SoftFOLInduction2] -> ShowS
show :: SoftFOLInduction2 -> String
$cshow :: SoftFOLInduction2 -> String
showsPrec :: Int -> SoftFOLInduction2 -> ShowS
$cshowsPrec :: Int -> SoftFOLInduction2 -> ShowS
Show

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

suleCFOL2SoftFOL :: GenSuleCFOL2SoftFOL PlainSoftFOL
suleCFOL2SoftFOL :: GenSuleCFOL2SoftFOL PlainSoftFOL
suleCFOL2SoftFOL = PlainSoftFOL -> GenSuleCFOL2SoftFOL PlainSoftFOL
forall a. a -> GenSuleCFOL2SoftFOL a
GenSuleCFOL2SoftFOL PlainSoftFOL
PlainSoftFOL

suleCFOL2SoftFOLInduction :: GenSuleCFOL2SoftFOL SoftFOLInduction
suleCFOL2SoftFOLInduction :: GenSuleCFOL2SoftFOL SoftFOLInduction
suleCFOL2SoftFOLInduction = SoftFOLInduction -> GenSuleCFOL2SoftFOL SoftFOLInduction
forall a. a -> GenSuleCFOL2SoftFOL a
GenSuleCFOL2SoftFOL SoftFOLInduction
SoftFOLInduction

suleCFOL2SoftFOLInduction2 :: GenSuleCFOL2SoftFOL SoftFOLInduction2
suleCFOL2SoftFOLInduction2 :: GenSuleCFOL2SoftFOL SoftFOLInduction2
suleCFOL2SoftFOLInduction2 = SoftFOLInduction2 -> GenSuleCFOL2SoftFOL SoftFOLInduction2
forall a. a -> GenSuleCFOL2SoftFOL a
GenSuleCFOL2SoftFOL SoftFOLInduction2
SoftFOLInduction2

-- | SoftFOL theories
type SoftFOLTheory = (SPSign.Sign, [Named SPTerm])

data CType = CSort
           | CVar SORT
           | CPred CSign.PredType
           | COp CSign.OpType
             deriving (CType -> CType -> Bool
(CType -> CType -> Bool) -> (CType -> CType -> Bool) -> Eq CType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CType -> CType -> Bool
$c/= :: CType -> CType -> Bool
== :: CType -> CType -> Bool
$c== :: CType -> CType -> Bool
Eq, Eq CType
Eq CType =>
(CType -> CType -> Ordering)
-> (CType -> CType -> Bool)
-> (CType -> CType -> Bool)
-> (CType -> CType -> Bool)
-> (CType -> CType -> Bool)
-> (CType -> CType -> CType)
-> (CType -> CType -> CType)
-> Ord CType
CType -> CType -> Bool
CType -> CType -> Ordering
CType -> CType -> CType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: CType -> CType -> CType
$cmin :: CType -> CType -> CType
max :: CType -> CType -> CType
$cmax :: CType -> CType -> CType
>= :: CType -> CType -> Bool
$c>= :: CType -> CType -> Bool
> :: CType -> CType -> Bool
$c> :: CType -> CType -> Bool
<= :: CType -> CType -> Bool
$c<= :: CType -> CType -> Bool
< :: CType -> CType -> Bool
$c< :: CType -> CType -> Bool
compare :: CType -> CType -> Ordering
$ccompare :: CType -> CType -> Ordering
$cp1Ord :: Eq CType
Ord, Int -> CType -> ShowS
[CType] -> ShowS
CType -> String
(Int -> CType -> ShowS)
-> (CType -> String) -> ([CType] -> ShowS) -> Show CType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CType] -> ShowS
$cshowList :: [CType] -> ShowS
show :: CType -> String
$cshow :: CType -> String
showsPrec :: Int -> CType -> ShowS
$cshowsPrec :: Int -> CType -> ShowS
Show)

toCKType :: CType -> CKType
toCKType :: CType -> CKType
toCKType ct :: CType
ct = case CType
ct of
  CSort -> CKType
CKSort
  CVar _ -> CKType
CKVar
  CPred _ -> CKType
CKPred
  COp _ -> CKType
CKOp

-- | CASL Ids with Types mapped to SPIdentifier
type IdTypeSPIdMap = Map.Map Id (Map.Map CType SPIdentifier)

-- | specialized lookup for IdTypeSPIdMap
lookupSPId :: Id -> CType -> IdTypeSPIdMap ->
          Maybe SPIdentifier
lookupSPId :: Id -> CType -> IdTypeSPIdMap -> Maybe SPIdentifier
lookupSPId i :: Id
i t :: CType
t = Maybe SPIdentifier
-> (Map CType SPIdentifier -> Maybe SPIdentifier)
-> Maybe (Map CType SPIdentifier)
-> Maybe SPIdentifier
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Maybe SPIdentifier
forall a. Maybe a
Nothing (CType -> Map CType SPIdentifier -> Maybe SPIdentifier
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup CType
t) (Maybe (Map CType SPIdentifier) -> Maybe SPIdentifier)
-> (IdTypeSPIdMap -> Maybe (Map CType SPIdentifier))
-> IdTypeSPIdMap
-> Maybe SPIdentifier
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> IdTypeSPIdMap -> Maybe (Map CType SPIdentifier)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i

-- | specialized insert (with error) for IdTypeSPIdMap
insertSPId :: Id -> CType ->
              SPIdentifier ->
              IdTypeSPIdMap ->
              IdTypeSPIdMap
insertSPId :: Id -> CType -> SPIdentifier -> IdTypeSPIdMap -> IdTypeSPIdMap
insertSPId i :: Id
i t :: CType
t spid :: SPIdentifier
spid m :: IdTypeSPIdMap
m =
    Bool -> IdTypeSPIdMap -> IdTypeSPIdMap
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (CKType -> String -> Bool
checkIdentifier (CType -> CKType
toCKType CType
t) (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
spid) (IdTypeSPIdMap -> IdTypeSPIdMap) -> IdTypeSPIdMap -> IdTypeSPIdMap
forall a b. (a -> b) -> a -> b
$
    (Map CType SPIdentifier
 -> Map CType SPIdentifier -> Map CType SPIdentifier)
-> Id -> Map CType SPIdentifier -> IdTypeSPIdMap -> IdTypeSPIdMap
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith ((SPIdentifier -> SPIdentifier -> SPIdentifier)
-> Map CType SPIdentifier
-> Map CType SPIdentifier
-> Map CType SPIdentifier
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith SPIdentifier -> SPIdentifier -> SPIdentifier
forall a. a
err) Id
i (CType
-> SPIdentifier -> Map CType SPIdentifier -> Map CType SPIdentifier
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert CType
t SPIdentifier
spid Map CType SPIdentifier
forall k a. Map k a
Map.empty) IdTypeSPIdMap
m
    where err :: a
err = String -> a
forall a. (?callStack::CallStack) => String -> a
error ("SuleCFOL2SoftFOL: for Id \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
i String -> ShowS
forall a. [a] -> [a] -> [a]
++
                       "\" the type \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ CType -> String
forall a. Show a => a -> String
show CType
t String -> ShowS
forall a. [a] -> [a] -> [a]
++
                       "\" can't be mapped to different SoftFOL identifiers")

deleteSPId :: Id -> CType ->
              IdTypeSPIdMap ->
              IdTypeSPIdMap
deleteSPId :: Id -> CType -> IdTypeSPIdMap -> IdTypeSPIdMap
deleteSPId i :: Id
i t :: CType
t m :: IdTypeSPIdMap
m =
    IdTypeSPIdMap
-> (Map CType SPIdentifier -> IdTypeSPIdMap)
-> Maybe (Map CType SPIdentifier)
-> IdTypeSPIdMap
forall b a. b -> (a -> b) -> Maybe a -> b
maybe IdTypeSPIdMap
m (\ m2 :: Map CType SPIdentifier
m2 -> let m2' :: Map CType SPIdentifier
m2' = CType -> Map CType SPIdentifier -> Map CType SPIdentifier
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete CType
t Map CType SPIdentifier
m2
                     in if Map CType SPIdentifier -> Bool
forall k a. Map k a -> Bool
Map.null Map CType SPIdentifier
m2'
                           then Id -> IdTypeSPIdMap -> IdTypeSPIdMap
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Id
i IdTypeSPIdMap
m
                           else Id -> Map CType SPIdentifier -> IdTypeSPIdMap -> IdTypeSPIdMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
i Map CType SPIdentifier
m2' IdTypeSPIdMap
m) (Maybe (Map CType SPIdentifier) -> IdTypeSPIdMap)
-> Maybe (Map CType SPIdentifier) -> IdTypeSPIdMap
forall a b. (a -> b) -> a -> b
$
          Id -> IdTypeSPIdMap -> Maybe (Map CType SPIdentifier)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i IdTypeSPIdMap
m

-- | specialized elems into a set for IdTypeSPIdMap
elemsSPIdSet :: IdTypeSPIdMap -> Set.Set SPIdentifier
elemsSPIdSet :: IdTypeSPIdMap -> Set SPIdentifier
elemsSPIdSet = (Map CType SPIdentifier -> Set SPIdentifier -> Set SPIdentifier)
-> Set SPIdentifier -> IdTypeSPIdMap -> Set SPIdentifier
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr (\ m :: Map CType SPIdentifier
m res :: Set SPIdentifier
res -> Set SPIdentifier -> Set SPIdentifier -> Set SPIdentifier
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set SPIdentifier
res
                                      ([SPIdentifier] -> Set SPIdentifier
forall a. Ord a => [a] -> Set a
Set.fromList (Map CType SPIdentifier -> [SPIdentifier]
forall k a. Map k a -> [a]
Map.elems Map CType SPIdentifier
m)))
                         Set SPIdentifier
forall a. Set a
Set.empty

-- extended signature translation
type SignTranslator f e = CSign.Sign f e -> e -> SoftFOLTheory -> SoftFOLTheory

-- extended signature translation for CASL
sigTrCASL :: SignTranslator () ()
sigTrCASL :: SignTranslator () ()
sigTrCASL _ _ = SoftFOLTheory -> SoftFOLTheory
forall a. a -> a
id

-- extended formula translation
type FormulaTranslator f e =
    CSign.Sign f e -> IdTypeSPIdMap -> f -> SPTerm

-- extended formula translation for CASL
formTrCASL :: FormulaTranslator () ()
formTrCASL :: FormulaTranslator () ()
formTrCASL _ _ = String -> () -> SPTerm
forall a. (?callStack::CallStack) => String -> a
error "SuleCFOL2SoftFOL: No extended formulas allowed in CASL"

instance Show a => Language (GenSuleCFOL2SoftFOL a) where
  language_name :: GenSuleCFOL2SoftFOL a -> String
language_name (GenSuleCFOL2SoftFOL a :: a
a) = "CASL2" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a

instance Show a => Comorphism (GenSuleCFOL2SoftFOL a)
               CASL CASL_Sublogics
               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CASLSign
               CASLMor
               CSign.Symbol RawSymbol ProofTree
               SoftFOL () [SPSign.TPTP] SPTerm () ()
               SPSign.Sign
               SoftFOLMorphism SFSymbol () ProofTree where
    sourceLogic :: GenSuleCFOL2SoftFOL a -> CASL
sourceLogic (GenSuleCFOL2SoftFOL _) = CASL
CASL
    sourceSublogic :: GenSuleCFOL2SoftFOL a -> CASL_Sublogics
sourceSublogic (GenSuleCFOL2SoftFOL a :: a
a) = CASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.cFol
                      { sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
LocFilSub
                      , cons_features :: SortGenerationFeatures
cons_features = SortGenerationFeatures
emptyMapConsFeature
                      , has_empty_sorts :: Bool
has_empty_sorts = a -> String
forall a. Show a => a -> String
show a
a String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== PlainSoftFOL -> String
forall a. Show a => a -> String
show PlainSoftFOL
PlainSoftFOL }
    sourceSublogicLossy :: GenSuleCFOL2SoftFOL a -> CASL_Sublogics
sourceSublogicLossy (GenSuleCFOL2SoftFOL a :: a
a) = CASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.fol
                      { sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
LocFilSub
                      , has_empty_sorts :: Bool
has_empty_sorts = a -> String
forall a. Show a => a -> String
show a
a String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== PlainSoftFOL -> String
forall a. Show a => a -> String
show PlainSoftFOL
PlainSoftFOL }
    targetLogic :: GenSuleCFOL2SoftFOL a -> SoftFOL
targetLogic (GenSuleCFOL2SoftFOL _) = SoftFOL
SoftFOL
    mapSublogic :: GenSuleCFOL2SoftFOL a -> CASL_Sublogics -> Maybe ()
mapSublogic cid :: GenSuleCFOL2SoftFOL a
cid sl :: CASL_Sublogics
sl =
        if CASL_Sublogics -> CASL_Sublogics -> Bool
forall l. SemiLatticeWithTop l => l -> l -> Bool
isSubElem CASL_Sublogics
sl (CASL_Sublogics -> Bool) -> CASL_Sublogics -> Bool
forall a b. (a -> b) -> a -> b
$ GenSuleCFOL2SoftFOL a -> 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 GenSuleCFOL2SoftFOL a
cid
        then () -> Maybe ()
forall a. a -> Maybe a
Just () else Maybe ()
forall a. Maybe a
Nothing
    map_theory :: GenSuleCFOL2SoftFOL a
-> (CASLSign, [Named CASLFORMULA]) -> Result SoftFOLTheory
map_theory (GenSuleCFOL2SoftFOL a :: a
a) = SignTranslator () ()
-> FormulaTranslator () ()
-> (CASLSign, [Named CASLFORMULA])
-> Result SoftFOLTheory
forall f e.
(FormExtension f, Eq f) =>
SignTranslator f e
-> FormulaTranslator f e
-> (Sign f e, [Named (FORMULA f)])
-> Result SoftFOLTheory
transTheory SignTranslator () ()
sigTrCASL FormulaTranslator () ()
formTrCASL
      ((CASLSign, [Named CASLFORMULA]) -> Result SoftFOLTheory)
-> ((CASLSign, [Named CASLFORMULA])
    -> (CASLSign, [Named CASLFORMULA]))
-> (CASLSign, [Named CASLFORMULA])
-> Result SoftFOLTheory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. case a -> String
forall a. Show a => a -> String
show a
a of
      str :: String
str | String
str String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== SoftFOLInduction -> String
forall a. Show a => a -> String
show SoftFOLInduction
SoftFOLInduction -> Bool
-> (CASLSign, [Named CASLFORMULA])
-> (CASLSign, [Named CASLFORMULA])
forall f e.
FormExtension f =>
Bool
-> (Sign f e, [Named (FORMULA f)])
-> (Sign f e, [Named (FORMULA f)])
generateInductionLemmas Bool
True
          | String
str String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== SoftFOLInduction2 -> String
forall a. Show a => a -> String
show SoftFOLInduction2
SoftFOLInduction2 -> Bool
-> (CASLSign, [Named CASLFORMULA])
-> (CASLSign, [Named CASLFORMULA])
forall f e.
FormExtension f =>
Bool
-> (Sign f e, [Named (FORMULA f)])
-> (Sign f e, [Named (FORMULA f)])
generateInductionLemmas Bool
False
          | Bool
otherwise -> (CASLSign, [Named CASLFORMULA]) -> (CASLSign, [Named CASLFORMULA])
forall a. a -> a
id
    extractModel :: GenSuleCFOL2SoftFOL a
-> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA])
extractModel (GenSuleCFOL2SoftFOL _) = CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA])
extractCASLModel
    has_model_expansion :: GenSuleCFOL2SoftFOL a -> Bool
has_model_expansion (GenSuleCFOL2SoftFOL _) = Bool
True

-- -------------------------- Signature -----------------------------

transFuncMap :: IdTypeSPIdMap ->
                CSign.Sign e f ->
                (FuncMap, IdTypeSPIdMap)
transFuncMap :: IdTypeSPIdMap -> Sign e f -> (FuncMap, IdTypeSPIdMap)
transFuncMap idMap :: IdTypeSPIdMap
idMap sign :: Sign e f
sign = (Id
 -> Set OpType
 -> (FuncMap, IdTypeSPIdMap)
 -> (FuncMap, IdTypeSPIdMap))
-> (FuncMap, IdTypeSPIdMap)
-> Map Id (Set OpType)
-> (FuncMap, IdTypeSPIdMap)
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey Id
-> Set OpType
-> (FuncMap, IdTypeSPIdMap)
-> (FuncMap, IdTypeSPIdMap)
toSPOpType (FuncMap
forall k a. Map k a
Map.empty, IdTypeSPIdMap
idMap)
  (Map Id (Set OpType) -> (FuncMap, IdTypeSPIdMap))
-> (MapSet Id OpType -> Map Id (Set OpType))
-> MapSet Id OpType
-> (FuncMap, IdTypeSPIdMap)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSet Id OpType -> Map Id (Set OpType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap (MapSet Id OpType -> (FuncMap, IdTypeSPIdMap))
-> MapSet Id OpType -> (FuncMap, IdTypeSPIdMap)
forall a b. (a -> b) -> a -> b
$ Sign e f -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
CSign.opMap Sign e f
sign
    where toSPOpType :: Id
-> Set OpType
-> (FuncMap, IdTypeSPIdMap)
-> (FuncMap, IdTypeSPIdMap)
toSPOpType iden :: Id
iden typeSet :: Set OpType
typeSet (fm :: FuncMap
fm, im :: IdTypeSPIdMap
im) =
              if Set OpType -> Bool
forall a. Set a -> Bool
isSingleton Set OpType
typeSet then
                 let oType :: OpType
oType = Set OpType -> OpType
forall a. Set a -> a
Set.findMin Set OpType
typeSet
                     sid' :: SPIdentifier
sid' = FuncMap -> OpType -> SPIdentifier
forall a. Map SPIdentifier a -> OpType -> SPIdentifier
sid FuncMap
fm OpType
oType
                 in (SPIdentifier
-> Set ([SPIdentifier], SPIdentifier) -> FuncMap -> FuncMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SPIdentifier
sid' (([SPIdentifier], SPIdentifier)
-> Set ([SPIdentifier], SPIdentifier)
forall a. a -> Set a
Set.singleton (OpType -> ([SPIdentifier], SPIdentifier)
transOpType OpType
oType)) FuncMap
fm,
                      Id -> CType -> SPIdentifier -> IdTypeSPIdMap -> IdTypeSPIdMap
insertSPId Id
iden (OpType -> CType
COp OpType
oType) SPIdentifier
sid' IdTypeSPIdMap
im)
              else (Set OpType
 -> (FuncMap, IdTypeSPIdMap) -> (FuncMap, IdTypeSPIdMap))
-> (FuncMap, IdTypeSPIdMap)
-> [Set OpType]
-> (FuncMap, IdTypeSPIdMap)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Set OpType -> (FuncMap, IdTypeSPIdMap) -> (FuncMap, IdTypeSPIdMap)
insOIdSet (FuncMap
fm, IdTypeSPIdMap
im)
                ([Set OpType] -> (FuncMap, IdTypeSPIdMap))
-> [Set OpType] -> (FuncMap, IdTypeSPIdMap)
forall a b. (a -> b) -> a -> b
$ (OpType -> OpType -> Bool) -> Set OpType -> [Set OpType]
forall a. Ord a => (a -> a -> Bool) -> Set a -> [Set a]
Rel.partSet (Sign e f -> OpType -> OpType -> Bool
forall f e. Sign f e -> OpType -> OpType -> Bool
leqF Sign e f
sign) Set OpType
typeSet
              where insOIdSet :: Set OpType -> (FuncMap, IdTypeSPIdMap) -> (FuncMap, IdTypeSPIdMap)
insOIdSet tset :: Set OpType
tset (fm' :: FuncMap
fm', im' :: IdTypeSPIdMap
im') =
                        let sid' :: SPIdentifier
sid' = FuncMap -> OpType -> SPIdentifier
forall a. Map SPIdentifier a -> OpType -> SPIdentifier
sid FuncMap
fm' (Set OpType -> OpType
forall a. Set a -> a
Set.findMax Set OpType
tset)
                        in (SPIdentifier
-> Set ([SPIdentifier], SPIdentifier) -> FuncMap -> FuncMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SPIdentifier
sid' ((OpType -> ([SPIdentifier], SPIdentifier))
-> Set OpType -> Set ([SPIdentifier], SPIdentifier)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map OpType -> ([SPIdentifier], SPIdentifier)
transOpType Set OpType
tset) FuncMap
fm',
                            (OpType -> IdTypeSPIdMap -> IdTypeSPIdMap)
-> IdTypeSPIdMap -> Set OpType -> IdTypeSPIdMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ x :: OpType
x -> Id -> CType -> SPIdentifier -> IdTypeSPIdMap -> IdTypeSPIdMap
insertSPId Id
iden (OpType -> CType
COp OpType
x) SPIdentifier
sid')
                                     IdTypeSPIdMap
im' Set OpType
tset)
                    sid :: Map SPIdentifier a -> OpType -> SPIdentifier
sid fma :: Map SPIdentifier a
fma t :: OpType
t = CKType
-> SPIdentifier
-> [SPIdentifier]
-> Set SPIdentifier
-> SPIdentifier
disSPOId CKType
CKOp (CKType -> Id -> SPIdentifier
transId CKType
CKOp Id
iden)
                                       (([SPIdentifier], SPIdentifier) -> [SPIdentifier]
forall a. ([a], a) -> [a]
uType (OpType -> ([SPIdentifier], SPIdentifier)
transOpType OpType
t))
                                       (Set SPIdentifier -> Set SPIdentifier -> Set SPIdentifier
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Map SPIdentifier a -> Set SPIdentifier
forall k a. Map k a -> Set k
Map.keysSet Map SPIdentifier a
fma)
                                           (IdTypeSPIdMap -> Set SPIdentifier
elemsSPIdSet IdTypeSPIdMap
idMap))
                    uType :: ([a], a) -> [a]
uType t :: ([a], a)
t = ([a], a) -> [a]
forall a b. (a, b) -> a
fst ([a], a)
t [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [([a], a) -> a
forall a b. (a, b) -> b
snd ([a], a)
t]

transPredMap :: IdTypeSPIdMap -> CSign.Sign e f
  -> (SPSign.PredMap, IdTypeSPIdMap)
transPredMap :: IdTypeSPIdMap -> Sign e f -> (PredMap, IdTypeSPIdMap)
transPredMap idMap :: IdTypeSPIdMap
idMap sign :: Sign e f
sign =
    (Id
 -> Set PredType
 -> (PredMap, IdTypeSPIdMap)
 -> (PredMap, IdTypeSPIdMap))
-> (PredMap, IdTypeSPIdMap)
-> Map Id (Set PredType)
-> (PredMap, IdTypeSPIdMap)
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey Id
-> Set PredType
-> (PredMap, IdTypeSPIdMap)
-> (PredMap, IdTypeSPIdMap)
toSPPredType (PredMap
forall k a. Map k a
Map.empty, IdTypeSPIdMap
idMap) (Map Id (Set PredType) -> (PredMap, IdTypeSPIdMap))
-> (MapSet Id PredType -> Map Id (Set PredType))
-> MapSet Id PredType
-> (PredMap, IdTypeSPIdMap)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSet Id PredType -> Map Id (Set PredType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap
      (MapSet Id PredType -> (PredMap, IdTypeSPIdMap))
-> MapSet Id PredType -> (PredMap, IdTypeSPIdMap)
forall a b. (a -> b) -> a -> b
$ Sign e f -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
CSign.predMap Sign e f
sign
    where toSPPredType :: Id
-> Set PredType
-> (PredMap, IdTypeSPIdMap)
-> (PredMap, IdTypeSPIdMap)
toSPPredType iden :: Id
iden typeSet :: Set PredType
typeSet (fm :: PredMap
fm, im :: IdTypeSPIdMap
im) =
              if Set PredType -> Bool
forall a. Set a -> Bool
isSingleton Set PredType
typeSet then
                let pType :: PredType
pType = Set PredType -> PredType
forall a. Set a -> a
Set.findMin Set PredType
typeSet
                    sid' :: SPIdentifier
sid' = PredMap -> PredType -> SPIdentifier
forall a. Map SPIdentifier a -> PredType -> SPIdentifier
sid PredMap
fm PredType
pType
                in (SPIdentifier -> Set [SPIdentifier] -> PredMap -> PredMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SPIdentifier
sid' ([SPIdentifier] -> Set [SPIdentifier]
forall a. a -> Set a
Set.singleton (PredType -> [SPIdentifier]
transPredType PredType
pType)) PredMap
fm
                   , Id -> CType -> SPIdentifier -> IdTypeSPIdMap -> IdTypeSPIdMap
insertSPId Id
iden (PredType -> CType
CPred PredType
pType) SPIdentifier
sid' IdTypeSPIdMap
im)
              else case -- genPredImplicationDisjunctions sign $
                        (PredType -> PredType -> Bool) -> Set PredType -> [Set PredType]
forall a. Ord a => (a -> a -> Bool) -> Set a -> [Set a]
Rel.partSet (Sign e f -> PredType -> PredType -> Bool
forall f e. Sign f e -> PredType -> PredType -> Bool
leqP Sign e f
sign) Set PredType
typeSet of
                     splitTySet :: [Set PredType]
splitTySet -> (Set PredType
 -> (PredMap, IdTypeSPIdMap) -> (PredMap, IdTypeSPIdMap))
-> (PredMap, IdTypeSPIdMap)
-> [Set PredType]
-> (PredMap, IdTypeSPIdMap)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Set PredType
-> (PredMap, IdTypeSPIdMap) -> (PredMap, IdTypeSPIdMap)
insOIdSet (PredMap
fm, IdTypeSPIdMap
im) [Set PredType]
splitTySet
              where insOIdSet :: Set PredType
-> (PredMap, IdTypeSPIdMap) -> (PredMap, IdTypeSPIdMap)
insOIdSet tset :: Set PredType
tset (fm' :: PredMap
fm', im' :: IdTypeSPIdMap
im') =
                        let sid' :: SPIdentifier
sid' = PredMap -> PredType -> SPIdentifier
forall a. Map SPIdentifier a -> PredType -> SPIdentifier
sid PredMap
fm' (Set PredType -> PredType
forall a. Set a -> a
Set.findMax Set PredType
tset)
                        in (SPIdentifier -> Set [SPIdentifier] -> PredMap -> PredMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SPIdentifier
sid' ((PredType -> [SPIdentifier]) -> Set PredType -> Set [SPIdentifier]
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map PredType -> [SPIdentifier]
transPredType Set PredType
tset) PredMap
fm',
                            (PredType -> IdTypeSPIdMap -> IdTypeSPIdMap)
-> IdTypeSPIdMap -> Set PredType -> IdTypeSPIdMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ x :: PredType
x -> Id -> CType -> SPIdentifier -> IdTypeSPIdMap -> IdTypeSPIdMap
insertSPId Id
iden (PredType -> CType
CPred PredType
x) SPIdentifier
sid')
                                     IdTypeSPIdMap
im' Set PredType
tset)
                    sid :: Map SPIdentifier a -> PredType -> SPIdentifier
sid fma :: Map SPIdentifier a
fma t :: PredType
t = CKType
-> SPIdentifier
-> [SPIdentifier]
-> Set SPIdentifier
-> SPIdentifier
disSPOId CKType
CKPred (CKType -> Id -> SPIdentifier
transId CKType
CKPred Id
iden)
                                       (PredType -> [SPIdentifier]
transPredType PredType
t)
                                       (Set SPIdentifier -> Set SPIdentifier -> Set SPIdentifier
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Map SPIdentifier a -> Set SPIdentifier
forall k a. Map k a -> Set k
Map.keysSet Map SPIdentifier a
fma)
                                           (IdTypeSPIdMap -> Set SPIdentifier
elemsSPIdSet IdTypeSPIdMap
idMap))

{- left typing implies right typing; explicit overloading sentences
are generated from these pairs, type TypePair = (CType,CType) -}

-- | disambiguation of SoftFOL Identifiers
disSPOId :: CKType -- ^ Type of CASl identifier
         -> SPIdentifier -- ^ translated CASL Identifier
         -> [SPIdentifier] {- ^ translated Sort Symbols of the profile
                           (maybe empty) -}
         -> Set.Set SPIdentifier -- ^ SoftFOL Identifiers already in use
         -> SPIdentifier {- ^ fresh Identifier generated from second argument;
    if the identifier was not in the set this is just the second argument -}
disSPOId :: CKType
-> SPIdentifier
-> [SPIdentifier]
-> Set SPIdentifier
-> SPIdentifier
disSPOId cType :: CKType
cType sid :: SPIdentifier
sid ty :: [SPIdentifier]
ty idSet :: Set SPIdentifier
idSet
    | CKType -> String -> Bool
checkIdentifier CKType
cType (SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
sid) Bool -> Bool -> Bool
&& Bool -> Bool
not (String -> Bool
lkup (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
sid) = SPIdentifier
sid
    | Bool
otherwise = let nSid :: String
nSid = ShowS
disSPOId' ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
sid
                  in Bool -> SPIdentifier -> SPIdentifier
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (CKType -> String -> Bool
checkIdentifier CKType
cType String
nSid) (SPIdentifier -> SPIdentifier) -> SPIdentifier -> SPIdentifier
forall a b. (a -> b) -> a -> b
$ String -> SPIdentifier
mkSimpleId String
nSid
    where disSPOId' :: ShowS
disSPOId' sid' :: String
sid'
              | Bool -> Bool
not (String -> Bool
lkup String
asid) = String
asid
              | Bool
otherwise = String -> Int -> String
addType String
asid 1
              where asid :: String
asid = String
sid' String -> ShowS
forall a. [a] -> [a] -> [a]
++ case CKType
cType of
                        CKSort -> ""
                        CKVar -> ""
                        x :: CKType
x -> '_' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show ([SPIdentifier] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SPIdentifier]
ty Int -> Int -> Int
forall a. Num a => a -> a -> a
- (case CKType
x of
                                                    CKOp -> 1
                                                    _ -> 0))
                    addType :: String -> Int -> String
addType res :: String
res n :: Int
n =
                        let nres :: String
nres = String
asid String -> ShowS
forall a. [a] -> [a] -> [a]
++ '_' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
fc Int
n
                            nres' :: String
nres' = String
nres String -> ShowS
forall a. [a] -> [a] -> [a]
++ '_' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
n
                        in if String
nres String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
res
                           then if String
nres' String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
res
                                then ShowS
forall a. (?callStack::CallStack) => String -> a
error ("SuleCFOL2SoftFOL: "
                                            String -> ShowS
forall a. [a] -> [a] -> [a]
++ "cannot calculate"
                                            String -> ShowS
forall a. [a] -> [a] -> [a]
++ " unambiguous id for "
                                            String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
sid String -> ShowS
forall a. [a] -> [a] -> [a]
++ " with type "
                                            String -> ShowS
forall a. [a] -> [a] -> [a]
++ [SPIdentifier] -> String
forall a. Show a => a -> String
show [SPIdentifier]
ty
                                            String -> ShowS
forall a. [a] -> [a] -> [a]
++ " and nres = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nres
                                            String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n with idSet "
                                            String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set SPIdentifier -> String
forall a. Show a => a -> String
show Set SPIdentifier
idSet)
                                else if Bool -> Bool
not (String -> Bool
lkup String
nres')
                                     then String
nres'
                                     else String -> Int -> String
addType String
nres (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
                           else if Bool -> Bool
not (String -> Bool
lkup String
nres)
                                then String
nres
                                else String -> Int -> String
addType String
nres (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
          lkup :: String -> Bool
lkup x :: String
x = SPIdentifier -> Set SPIdentifier -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (String -> SPIdentifier
mkSimpleId String
x) Set SPIdentifier
idSet
          fc :: Int -> String
fc n :: Int
n = (SPIdentifier -> String) -> [SPIdentifier] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Int -> ShowS
forall a. Int -> [a] -> [a]
take Int
n ShowS -> (SPIdentifier -> String) -> SPIdentifier -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPIdentifier -> String
forall a. Show a => a -> String
show) [SPIdentifier]
ty

transOpType :: CSign.OpType -> ([SPIdentifier], SPIdentifier)
transOpType :: OpType -> ([SPIdentifier], SPIdentifier)
transOpType ot :: OpType
ot = ((Id -> SPIdentifier) -> [Id] -> [SPIdentifier]
forall a b. (a -> b) -> [a] -> [b]
map Id -> SPIdentifier
transIdSort (OpType -> [Id]
CSign.opArgs OpType
ot),
                  Id -> SPIdentifier
transIdSort (OpType -> Id
CSign.opRes OpType
ot))

transPredType :: CSign.PredType -> [SPIdentifier]
transPredType :: PredType -> [SPIdentifier]
transPredType = (Id -> SPIdentifier) -> [Id] -> [SPIdentifier]
forall a b. (a -> b) -> [a] -> [b]
map Id -> SPIdentifier
transIdSort ([Id] -> [SPIdentifier])
-> (PredType -> [Id]) -> PredType -> [SPIdentifier]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> [Id]
CSign.predArgs

-- | translate every Id as Sort
transIdSort :: Id -> SPIdentifier
transIdSort :: Id -> SPIdentifier
transIdSort = CKType -> Id -> SPIdentifier
transId CKType
CKSort

integrateGenerated :: IdTypeSPIdMap -> [Named (FORMULA f)] ->
                      SPSign.Sign ->
                      Result (IdTypeSPIdMap, SPSign.Sign, [Named SPTerm])
integrateGenerated :: IdTypeSPIdMap
-> [Named (FORMULA f)]
-> Sign
-> Result (IdTypeSPIdMap, Sign, [Named SPTerm])
integrateGenerated idMap :: IdTypeSPIdMap
idMap genSens :: [Named (FORMULA f)]
genSens sign :: Sign
sign
    | [Named (FORMULA f)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Named (FORMULA f)]
genSens = (IdTypeSPIdMap, Sign, [Named SPTerm])
-> Result (IdTypeSPIdMap, Sign, [Named SPTerm])
forall (m :: * -> *) a. Monad m => a -> m a
return (IdTypeSPIdMap
idMap, Sign
sign, [])
    | Bool
otherwise =
      case (Named (FORMULA f) -> Bool)
-> [Named (FORMULA f)]
-> ([Named (FORMULA f)], [Named (FORMULA f)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Named (FORMULA f) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom [Named (FORMULA f)]
genSens of
      (genAxs :: [Named (FORMULA f)]
genAxs, genGoals :: [Named (FORMULA f)]
genGoals) ->
        case Sign
-> IdTypeSPIdMap
-> [Named (FORMULA f)]
-> (PredMap, IdTypeSPIdMap, [Named SPTerm])
forall f.
Sign
-> IdTypeSPIdMap
-> [Named (FORMULA f)]
-> (PredMap, IdTypeSPIdMap, [Named SPTerm])
makeGenGoals Sign
sign IdTypeSPIdMap
idMap [Named (FORMULA f)]
genGoals of
        (newPredsMap :: PredMap
newPredsMap, idMap' :: IdTypeSPIdMap
idMap', goalsAndSentences :: [Named SPTerm]
goalsAndSentences) ->
          -- makeGens must not invent new sorts
          case Sign
-> IdTypeSPIdMap
-> [Named (FORMULA f)]
-> Result (SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm])
forall f.
Sign
-> IdTypeSPIdMap
-> [Named (FORMULA f)]
-> Result (SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm])
makeGens Sign
sign IdTypeSPIdMap
idMap' [Named (FORMULA f)]
genAxs of
          Result dias :: [Diagnosis]
dias mv :: Maybe (SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm])
mv ->
            Result (IdTypeSPIdMap, Sign, [Named SPTerm])
-> ((SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm])
    -> Result (IdTypeSPIdMap, Sign, [Named SPTerm]))
-> Maybe (SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm])
-> Result (IdTypeSPIdMap, Sign, [Named SPTerm])
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Diagnosis]
-> Maybe (IdTypeSPIdMap, Sign, [Named SPTerm])
-> Result (IdTypeSPIdMap, Sign, [Named SPTerm])
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
dias Maybe (IdTypeSPIdMap, Sign, [Named SPTerm])
forall a. Maybe a
Nothing)
                  (\ (spSortMap_makeGens :: SortMap
spSortMap_makeGens, newOpsMap :: FuncMap
newOpsMap, idMap'' :: IdTypeSPIdMap
idMap'', exhaustSens :: [Named SPTerm]
exhaustSens) ->
                      let spSortMap' :: SortMap
spSortMap' =
                            SortMap -> SortMap -> SortMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union SortMap
spSortMap_makeGens (Sign -> SortMap
SPSign.sortMap Sign
sign)
                      in Bool
-> Result (IdTypeSPIdMap, Sign, [Named SPTerm])
-> Result (IdTypeSPIdMap, Sign, [Named SPTerm])
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (SortMap -> Int
forall k a. Map k a -> Int
Map.size SortMap
spSortMap' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==
                                    SortMap -> Int
forall k a. Map k a -> Int
Map.size (Sign -> SortMap
SPSign.sortMap Sign
sign))
                             ([Diagnosis]
-> Maybe (IdTypeSPIdMap, Sign, [Named SPTerm])
-> Result (IdTypeSPIdMap, Sign, [Named SPTerm])
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
dias
                                     ((IdTypeSPIdMap, Sign, [Named SPTerm])
-> Maybe (IdTypeSPIdMap, Sign, [Named SPTerm])
forall a. a -> Maybe a
Just (IdTypeSPIdMap
idMap'',
                                            Sign
sign { sortMap :: SortMap
sortMap = SortMap
spSortMap'
                                                 , funcMap :: FuncMap
funcMap =
                                                     FuncMap -> FuncMap -> FuncMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (Sign -> FuncMap
funcMap Sign
sign)
                                                               FuncMap
newOpsMap
                                                 , predMap :: PredMap
SPSign.predMap =
                                                     PredMap -> PredMap -> PredMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union
                                                     (Sign -> PredMap
SPSign.predMap Sign
sign)
                                                               PredMap
newPredsMap},
                                            IdTypeSPIdMap -> FuncMap -> [Named SPTerm]
mkInjSentences IdTypeSPIdMap
idMap' FuncMap
newOpsMap [Named SPTerm] -> [Named SPTerm] -> [Named SPTerm]
forall a. [a] -> [a] -> [a]
++
                                            [Named SPTerm]
goalsAndSentences [Named SPTerm] -> [Named SPTerm] -> [Named SPTerm]
forall a. [a] -> [a] -> [a]
++
                                            [Named SPTerm]
exhaustSens))))
                  Maybe (SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm])
mv

makeGenGoals :: SPSign.Sign -> IdTypeSPIdMap -> [Named (FORMULA f)]
             -> (SPSign.PredMap, IdTypeSPIdMap, [Named SPTerm])
makeGenGoals :: Sign
-> IdTypeSPIdMap
-> [Named (FORMULA f)]
-> (PredMap, IdTypeSPIdMap, [Named SPTerm])
makeGenGoals sign :: Sign
sign idMap :: IdTypeSPIdMap
idMap fs :: [Named (FORMULA f)]
fs =
  let Result _ res :: Maybe (SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm])
res = Sign
-> IdTypeSPIdMap
-> [Named (FORMULA f)]
-> Result (SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm])
forall f.
Sign
-> IdTypeSPIdMap
-> [Named (FORMULA f)]
-> Result (SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm])
makeGens Sign
sign IdTypeSPIdMap
idMap [Named (FORMULA f)]
fs
  in case Maybe (SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm])
res of
   Nothing -> (PredMap
forall k a. Map k a
Map.empty, IdTypeSPIdMap
idMap, [])
   Just (_, _, idMap' :: IdTypeSPIdMap
idMap', fs' :: [Named SPTerm]
fs') ->
     let fs'' :: [Named SPTerm]
fs'' = (Named SPTerm -> Named SPTerm) -> [Named SPTerm] -> [Named SPTerm]
forall a b. (a -> b) -> [a] -> [b]
map (\ s :: Named SPTerm
s -> Named SPTerm
s {isAxiom :: Bool
isAxiom = Bool
False}) [Named SPTerm]
fs'
     in (PredMap
forall k a. Map k a
Map.empty, IdTypeSPIdMap
idMap', [Named SPTerm]
fs'')
 {- Sort_gen_ax as goals only implemented through a hack."
sketch of full implementation :
   - invent new predicate P that is supposed to hold on
     every x in the (freely) generated sort.
   - generate formulas with this predicate for each constructor.
   - recursive constructors hold if the predicate holds on the variables
   - prove forall x . P(x)

  implementation is postponed as this translation does not produce
only one goal, but additional symbols, axioms and a goal
 -}

makeGens :: SPSign.Sign -> IdTypeSPIdMap -> [Named (FORMULA f)]
         -> Result (SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm])
            {- ^ The list of SoftFOL sentences gives exhaustiveness for
            generated sorts with only constant constructors
            and\/or subsort injections, by simply translating
            such sort generation constraints to disjunctions -}
makeGens :: Sign
-> IdTypeSPIdMap
-> [Named (FORMULA f)]
-> Result (SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm])
makeGens sign :: Sign
sign idMap :: IdTypeSPIdMap
idMap fs :: [Named (FORMULA f)]
fs =
    case (Result
   (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
    [Named SPTerm])
 -> Named (FORMULA f)
 -> Result
      (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
       [Named SPTerm]))
-> Result
     (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
      [Named SPTerm])
-> [Named (FORMULA f)]
-> Result
     (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
      [Named SPTerm])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Sign
-> Result
     (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
      [Named SPTerm])
-> Named (FORMULA f)
-> Result
     (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
      [Named SPTerm])
forall f.
Sign
-> Result
     (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
      [Named SPTerm])
-> Named (FORMULA f)
-> Result
     (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
      [Named SPTerm])
makeGen Sign
sign) ((FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
 [Named SPTerm])
-> Result
     (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
      [Named SPTerm])
forall (m :: * -> *) a. Monad m => a -> m a
return (FuncMap
forall k a. Map k a
Map.empty, IdTypeSPIdMap
idMap, [], [])) [Named (FORMULA f)]
fs of
    Result ds :: [Diagnosis]
ds mv :: Maybe
  (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
   [Named SPTerm])
mv ->
        Result (SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm])
-> ((FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
     [Named SPTerm])
    -> Result (SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm]))
-> Maybe
     (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
      [Named SPTerm])
-> Result (SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm])
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Diagnosis]
-> Maybe (SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm])
-> Result (SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm])
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds Maybe (SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm])
forall a. Maybe a
Nothing)
              (\ (opM :: FuncMap
opM, idMap' :: IdTypeSPIdMap
idMap', pairs :: [(SPIdentifier, Maybe Generated)]
pairs, exhaustSens :: [Named SPTerm]
exhaustSens) ->
                   [Diagnosis]
-> Maybe (SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm])
-> Result (SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm])
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds
                      ((SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm])
-> Maybe (SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm])
forall a. a -> Maybe a
Just (((SPIdentifier, Maybe Generated) -> SortMap -> SortMap)
-> SortMap -> [(SPIdentifier, Maybe Generated)] -> SortMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((SPIdentifier -> Maybe Generated -> SortMap -> SortMap)
-> (SPIdentifier, Maybe Generated) -> SortMap -> SortMap
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SPIdentifier -> Maybe Generated -> SortMap -> SortMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert)
                                   SortMap
forall k a. Map k a
Map.empty [(SPIdentifier, Maybe Generated)]
pairs,
                             FuncMap
opM, IdTypeSPIdMap
idMap', [Named SPTerm]
exhaustSens)))
              Maybe
  (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
   [Named SPTerm])
mv

makeGen :: SPSign.Sign
        -> Result (FuncMap, IdTypeSPIdMap,
                   [(SPIdentifier, Maybe Generated)], [Named SPTerm])
        -> Named (FORMULA f)
        -> Result (FuncMap, IdTypeSPIdMap,
                   [(SPIdentifier, Maybe Generated)], [Named SPTerm])
makeGen :: Sign
-> Result
     (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
      [Named SPTerm])
-> Named (FORMULA f)
-> Result
     (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
      [Named SPTerm])
makeGen sign :: Sign
sign r :: Result
  (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
   [Named SPTerm])
r@(Result ods :: [Diagnosis]
ods omv :: Maybe
  (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
   [Named SPTerm])
omv) nf :: Named (FORMULA f)
nf =
    Result
  (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
   [Named SPTerm])
-> ((FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
     [Named SPTerm])
    -> Result
         (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
          [Named SPTerm]))
-> Maybe
     (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
      [Named SPTerm])
-> Result
     (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
      [Named SPTerm])
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Diagnosis]
-> Maybe
     (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
      [Named SPTerm])
-> Result
     (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
      [Named SPTerm])
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ods Maybe
  (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
   [Named SPTerm])
forall a. Maybe a
Nothing) (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
 [Named SPTerm])
-> Result
     (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
      [Named SPTerm])
process Maybe
  (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
   [Named SPTerm])
omv where
 process :: (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
 [Named SPTerm])
-> Result
     (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
      [Named SPTerm])
process (oMap :: FuncMap
oMap, iMap :: IdTypeSPIdMap
iMap, rList :: [(SPIdentifier, Maybe Generated)]
rList, eSens :: [Named SPTerm]
eSens) = case Named (FORMULA f) -> FORMULA f
forall s a. SenAttr s a -> s
sentence Named (FORMULA f)
nf of
  Sort_gen_ax constrs :: [Constraint]
constrs free :: Bool
free ->
      if [(Id, Id)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Id, Id)]
mp then (case ((FuncMap, IdTypeSPIdMap, [Named SPTerm])
 -> Id
 -> ((FuncMap, IdTypeSPIdMap, [Named SPTerm]),
     (SPIdentifier, Maybe Generated)))
-> (FuncMap, IdTypeSPIdMap, [Named SPTerm])
-> [Id]
-> ((FuncMap, IdTypeSPIdMap, [Named SPTerm]),
    [(SPIdentifier, Maybe Generated)])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL (FuncMap, IdTypeSPIdMap, [Named SPTerm])
-> Id
-> ((FuncMap, IdTypeSPIdMap, [Named SPTerm]),
    (SPIdentifier, Maybe Generated))
makeGenP (FuncMap
oMap, IdTypeSPIdMap
iMap, []) [Id]
srts of
                       ((oMap' :: FuncMap
oMap', iMap' :: IdTypeSPIdMap
iMap', eSens' :: [Named SPTerm]
eSens'), genPairs :: [(SPIdentifier, Maybe Generated)]
genPairs) ->
                          [Diagnosis]
-> Maybe
     (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
      [Named SPTerm])
-> Result
     (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
      [Named SPTerm])
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ods ((FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
 [Named SPTerm])
-> Maybe
     (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
      [Named SPTerm])
forall a. a -> Maybe a
Just (FuncMap
oMap', IdTypeSPIdMap
iMap',
                                            [(SPIdentifier, Maybe Generated)]
rList [(SPIdentifier, Maybe Generated)]
-> [(SPIdentifier, Maybe Generated)]
-> [(SPIdentifier, Maybe Generated)]
forall a. [a] -> [a] -> [a]
++ [(SPIdentifier, Maybe Generated)]
genPairs,
                                            [Named SPTerm]
eSens [Named SPTerm] -> [Named SPTerm] -> [Named SPTerm]
forall a. [a] -> [a] -> [a]
++ [Named SPTerm]
eSens')))
                 else String
-> [(Id, Id)]
-> Result
     (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
      [Named SPTerm])
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError ("Sort generation constraints with " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                               "non-injective sort mappings cannot " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                               "be translated to SoftFOL") [(Id, Id)]
mp
      where -- compute standard form of sort generation constraints
            (srts :: [Id]
srts, ops :: [OP_SYMB]
ops, mp :: [(Id, Id)]
mp) = [Constraint] -> ([Id], [OP_SYMB], [(Id, Id)])
recover_Sort_gen_ax [Constraint]
constrs
            -- test whether a constructor belongs to a specific sort
            hasTheSort :: Id -> OP_SYMB -> Bool
hasTheSort s :: Id
s (Qual_op_name _ ot :: OP_TYPE
ot _) = Id
s Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== OP_TYPE -> Id
res_OP_TYPE OP_TYPE
ot
            hasTheSort _ _ = String -> Bool
forall a. (?callStack::CallStack) => String -> a
error "SuleCFOL2SoftFOL.hasTheSort"
            mkGen :: [(SPIdentifier, b)] -> Maybe Generated
mkGen = Generated -> Maybe Generated
forall a. a -> Maybe a
Just (Generated -> Maybe Generated)
-> ([(SPIdentifier, b)] -> Generated)
-> [(SPIdentifier, b)]
-> Maybe Generated
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> [SPIdentifier] -> Generated
Generated Bool
free ([SPIdentifier] -> Generated)
-> ([(SPIdentifier, b)] -> [SPIdentifier])
-> [(SPIdentifier, b)]
-> Generated
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SPIdentifier, b) -> SPIdentifier)
-> [(SPIdentifier, b)] -> [SPIdentifier]
forall a b. (a -> b) -> [a] -> [b]
map (SPIdentifier, b) -> SPIdentifier
forall a b. (a, b) -> a
fst
            -- translate constraint for one sort
            makeGenP :: (FuncMap, IdTypeSPIdMap, [Named SPTerm])
-> Id
-> ((FuncMap, IdTypeSPIdMap, [Named SPTerm]),
    (SPIdentifier, Maybe Generated))
makeGenP (opM :: FuncMap
opM, idMap :: IdTypeSPIdMap
idMap, exSens :: [Named SPTerm]
exSens) s :: Id
s = ((FuncMap
newOpMap, IdTypeSPIdMap
newIdMap,
                                                [Named SPTerm]
exSens [Named SPTerm] -> [Named SPTerm] -> [Named SPTerm]
forall a. [a] -> [a] -> [a]
++ [OP_SYMB] -> Id -> [Named SPTerm]
eSen [OP_SYMB]
ops_of_s Id
s),
                                        (SPIdentifier
s', [(SPIdentifier, ([SPIdentifier], SPIdentifier))] -> Maybe Generated
forall b. [(SPIdentifier, b)] -> Maybe Generated
mkGen [(SPIdentifier, ([SPIdentifier], SPIdentifier))]
cons))
                where ((newOpMap :: FuncMap
newOpMap, newIdMap :: IdTypeSPIdMap
newIdMap), cons :: [(SPIdentifier, ([SPIdentifier], SPIdentifier))]
cons) =
                          ((FuncMap, IdTypeSPIdMap)
 -> OP_SYMB
 -> ((FuncMap, IdTypeSPIdMap),
     (SPIdentifier, ([SPIdentifier], SPIdentifier))))
-> (FuncMap, IdTypeSPIdMap)
-> [OP_SYMB]
-> ((FuncMap, IdTypeSPIdMap),
    [(SPIdentifier, ([SPIdentifier], SPIdentifier))])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL (FuncMap, IdTypeSPIdMap)
-> OP_SYMB
-> ((FuncMap, IdTypeSPIdMap),
    (SPIdentifier, ([SPIdentifier], SPIdentifier)))
mkInjOp (FuncMap
opM, IdTypeSPIdMap
idMap) [OP_SYMB]
ops_of_s
                      ops_of_s :: [OP_SYMB]
ops_of_s = (OP_SYMB -> Bool) -> [OP_SYMB] -> [OP_SYMB]
forall a. (a -> Bool) -> [a] -> [a]
List.filter (Id -> OP_SYMB -> Bool
hasTheSort Id
s) [OP_SYMB]
ops
                      s' :: SPIdentifier
s' = SPIdentifier -> Maybe SPIdentifier -> SPIdentifier
forall a. a -> Maybe a -> a
fromMaybe (String -> SPIdentifier
forall a. (?callStack::CallStack) => String -> a
error (String -> SPIdentifier) -> String -> SPIdentifier
forall a b. (a -> b) -> a -> b
$ "SuleCFOL2SoftFOL.makeGen: "
                                        String -> ShowS
forall a. [a] -> [a] -> [a]
++ "No mapping found for '"
                                        String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> ShowS
forall a. Show a => a -> ShowS
shows Id
s "'")
                                 (Id -> CType -> IdTypeSPIdMap -> Maybe SPIdentifier
lookupSPId Id
s CType
CSort IdTypeSPIdMap
idMap)
            {- is an operation a constant or an injection ?
            (we currently can translate only these) -}
            isConstorInj :: OP_SYMB -> Bool
isConstorInj o :: OP_SYMB
o =
              OP_SYMB -> Bool
nullArgs OP_SYMB
o Bool -> Bool -> Bool
|| Id -> Bool
isInjName (OP_SYMB -> Id
opSymbName OP_SYMB
o)
            -- generate sentences for one sort
            eSen :: [OP_SYMB] -> Id -> [Named SPTerm]
eSen os :: [OP_SYMB]
os s :: Id
s = [ String -> SPTerm -> Named SPTerm
forall a s. a -> s -> SenAttr s a
makeNamed (Id -> String
forall a. Pretty a => a -> String
newName Id
s) (SPQuantSym -> [SPTerm] -> SPTerm -> SPTerm
SPQuantTerm SPQuantSym
SPForall
                            [SPIdentifier -> SPIdentifier -> SPTerm
typedVarTerm SPIdentifier
var1
                             (SPIdentifier -> SPTerm) -> SPIdentifier -> SPTerm
forall a b. (a -> b) -> a -> b
$ SPIdentifier -> Maybe SPIdentifier -> SPIdentifier
forall a. a -> Maybe a -> a
fromMaybe (String -> SPIdentifier
forall a. (?callStack::CallStack) => String -> a
error "lookup failed")
                             (Id -> CType -> IdTypeSPIdMap -> Maybe SPIdentifier
lookupSPId Id
s CType
CSort IdTypeSPIdMap
iMap)] (SPIdentifier -> [OP_SYMB] -> SPTerm
disj SPIdentifier
var1 [OP_SYMB]
os))
                        | (OP_SYMB -> Bool) -> [OP_SYMB] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all OP_SYMB -> Bool
isConstorInj [OP_SYMB]
os ]
            -- generate sentences: compute one disjunct (for one alternative)
            mkDisjunct :: SPIdentifier -> OP_SYMB -> SPTerm
mkDisjunct v :: SPIdentifier
v o :: OP_SYMB
o@(Qual_op_name _ (Op_type _ args :: [Id]
args res :: Id
res _) _) =
              -- a constant? then just compare with it
              case [Id]
args of
                [] -> SPTerm -> SPTerm -> SPTerm
mkEq (SPIdentifier -> SPTerm
varTerm SPIdentifier
v) (SPTerm -> SPTerm) -> SPTerm -> SPTerm
forall a b. (a -> b) -> a -> b
$ SPIdentifier -> SPTerm
varTerm (SPIdentifier -> SPTerm) -> SPIdentifier -> SPTerm
forall a b. (a -> b) -> a -> b
$ IdTypeSPIdMap -> OP_SYMB -> SPIdentifier
transOPSYMB IdTypeSPIdMap
iMap OP_SYMB
o
                {- an injection? then quantify existentially
                (for the injection's argument)
                since injections are identities, we can leave them out -}
                [arg :: Id
arg] -> let ta :: SPIdentifier
ta = Id -> SPIdentifier
transIdSort Id
arg in SPQuantSym -> [SPTerm] -> SPTerm -> SPTerm
SPQuantTerm SPQuantSym
SPExists
                  [ SPIdentifier -> SPIdentifier -> SPTerm
typedVarTerm SPIdentifier
var2 SPIdentifier
ta ]
                   (SPTerm -> SPTerm) -> SPTerm -> SPTerm
forall a b. (a -> b) -> a -> b
$ SPTerm -> SPTerm -> SPTerm
mkEq (SPIdentifier -> SPTerm
varTerm SPIdentifier
v)
                   (SPTerm -> SPTerm) -> SPTerm -> SPTerm
forall a b. (a -> b) -> a -> b
$ if SPIdentifier -> SPIdentifier -> Rel SPIdentifier -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.member SPIdentifier
ta (Id -> SPIdentifier
transIdSort Id
res)
                        (Rel SPIdentifier -> Bool) -> Rel SPIdentifier -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Rel SPIdentifier
SPSign.sortRel Sign
sign
                     then SPIdentifier -> SPTerm
varTerm SPIdentifier
var2
                     else SPSymbol -> [SPTerm] -> SPTerm
compTerm (SPIdentifier -> SPSymbol
spSym (SPIdentifier -> SPSymbol) -> SPIdentifier -> SPSymbol
forall a b. (a -> b) -> a -> b
$ IdTypeSPIdMap -> OP_SYMB -> SPIdentifier
transOPSYMB IdTypeSPIdMap
iMap OP_SYMB
o) [SPIdentifier -> SPTerm
varTerm SPIdentifier
var2]
                _ -> String -> SPTerm
forall a. (?callStack::CallStack) => String -> a
error "cannot handle ordinary constructors"
            mkDisjunct _ _ = String -> SPTerm
forall a. (?callStack::CallStack) => String -> a
error "unqualified operation symbol"
            -- make disjunction out of all the alternatives
            disj :: SPIdentifier -> [OP_SYMB] -> SPTerm
disj v :: SPIdentifier
v os :: [OP_SYMB]
os = case (OP_SYMB -> SPTerm) -> [OP_SYMB] -> [SPTerm]
forall a b. (a -> b) -> [a] -> [b]
map (SPIdentifier -> OP_SYMB -> SPTerm
mkDisjunct SPIdentifier
v) [OP_SYMB]
os of
                        [] -> String -> SPTerm
forall a. (?callStack::CallStack) => String -> a
error "SuleCFOL2SoftFOL: no constructors found"
                        [x :: SPTerm
x] -> SPTerm
x
                        xs :: [SPTerm]
xs -> (SPTerm -> SPTerm -> SPTerm) -> [SPTerm] -> SPTerm
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 SPTerm -> SPTerm -> SPTerm
mkDisj [SPTerm]
xs
            -- generate enough variables
            var :: String
var = Maybe String -> String
forall a. (?callStack::CallStack) => Maybe a -> a
fromJust ((String -> Bool) -> [String] -> Maybe String
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\ x :: String
x ->
                      Bool -> Bool
not (SPIdentifier -> Set SPIdentifier -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (String -> SPIdentifier
mkSimpleId String
x) Set SPIdentifier
usedIds))
                            ("X" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: ['X' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
i | Int
i <- [(1 :: Int) ..]]))
            var1 :: SPIdentifier
var1 = String -> SPIdentifier
mkSimpleId String
var
            var2 :: SPIdentifier
var2 = String -> SPIdentifier
mkSimpleId (String -> SPIdentifier) -> String -> SPIdentifier
forall a b. (a -> b) -> a -> b
$ String
var String -> ShowS
forall a. [a] -> [a] -> [a]
++ "a"
            varTerm :: SPIdentifier -> SPTerm
varTerm = SPSymbol -> SPTerm
simpTerm (SPSymbol -> SPTerm)
-> (SPIdentifier -> SPSymbol) -> SPIdentifier -> SPTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPIdentifier -> SPSymbol
spSym
            newName :: a -> String
newName s :: a
s = "ga_exhaustive_generated_sort_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (a -> Doc
forall a. Pretty a => a -> Doc
pretty a
s)
            usedIds :: Set SPIdentifier
usedIds = IdTypeSPIdMap -> Set SPIdentifier
elemsSPIdSet IdTypeSPIdMap
iMap
            nullArgs :: OP_SYMB -> Bool
nullArgs o :: OP_SYMB
o = case OP_SYMB
o of
                         Qual_op_name _ (Op_type _ args :: [Id]
args _ _) _ -> [Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
args
                         _ -> String -> Bool
forall a. (?callStack::CallStack) => String -> a
error "SuleCFOL2SoftFOL: wrong constructor"
  _ -> Result
  (FuncMap, IdTypeSPIdMap, [(SPIdentifier, Maybe Generated)],
   [Named SPTerm])
r

mkInjOp :: (FuncMap, IdTypeSPIdMap)
        -> OP_SYMB
        -> ((FuncMap, IdTypeSPIdMap),
            (SPIdentifier, ([SPIdentifier], SPIdentifier)))
mkInjOp :: (FuncMap, IdTypeSPIdMap)
-> OP_SYMB
-> ((FuncMap, IdTypeSPIdMap),
    (SPIdentifier, ([SPIdentifier], SPIdentifier)))
mkInjOp (opM :: FuncMap
opM, idMap :: IdTypeSPIdMap
idMap) qo :: OP_SYMB
qo@(Qual_op_name i :: Id
i ot :: OP_TYPE
ot _) =
    if Id -> Bool
isInjName Id
i Bool -> Bool -> Bool
&& Maybe SPIdentifier -> Bool
forall a. Maybe a -> Bool
isNothing Maybe SPIdentifier
lsid
       then ((SPIdentifier
-> Set ([SPIdentifier], SPIdentifier) -> FuncMap -> FuncMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SPIdentifier
i' (([SPIdentifier], SPIdentifier)
-> Set ([SPIdentifier], SPIdentifier)
forall a. a -> Set a
Set.singleton (OpType -> ([SPIdentifier], SPIdentifier)
transOpType OpType
ot')) FuncMap
opM,
              Id -> CType -> SPIdentifier -> IdTypeSPIdMap -> IdTypeSPIdMap
insertSPId Id
i (OpType -> CType
COp OpType
ot') SPIdentifier
i' IdTypeSPIdMap
idMap),
             (SPIdentifier
i', OpType -> ([SPIdentifier], SPIdentifier)
transOpType OpType
ot'))
       else ((FuncMap
opM, IdTypeSPIdMap
idMap),
             (SPIdentifier -> Maybe SPIdentifier -> SPIdentifier
forall a. a -> Maybe a -> a
fromMaybe SPIdentifier
forall a. a
err Maybe SPIdentifier
lsid,
              OpType -> ([SPIdentifier], SPIdentifier)
transOpType OpType
ot'))
    where i' :: SPIdentifier
i' = CKType
-> SPIdentifier
-> [SPIdentifier]
-> Set SPIdentifier
-> SPIdentifier
disSPOId CKType
CKOp (CKType -> Id -> SPIdentifier
transId CKType
CKOp Id
i)
                        (([SPIdentifier], SPIdentifier) -> [SPIdentifier]
forall a. ([a], a) -> [a]
utype (OpType -> ([SPIdentifier], SPIdentifier)
transOpType OpType
ot')) Set SPIdentifier
usedNames
          ot' :: OpType
ot' = OP_TYPE -> OpType
CSign.toOpType OP_TYPE
ot
          lsid :: Maybe SPIdentifier
lsid = Id -> CType -> IdTypeSPIdMap -> Maybe SPIdentifier
lookupSPId Id
i (OpType -> CType
COp OpType
ot') IdTypeSPIdMap
idMap
          usedNames :: Set SPIdentifier
usedNames = FuncMap -> Set SPIdentifier
forall k a. Map k a -> Set k
Map.keysSet FuncMap
opM
          err :: a
err = String -> a
forall a. (?callStack::CallStack) => String -> a
error ("SuleCFOL2SoftFOL.mkInjOp: Cannot find SPId for '"
                       String -> ShowS
forall a. [a] -> [a] -> [a]
++ OP_SYMB -> String
forall a. Show a => a -> String
show OP_SYMB
qo String -> ShowS
forall a. [a] -> [a] -> [a]
++ "'")
          utype :: ([a], a) -> [a]
utype t :: ([a], a)
t = ([a], a) -> [a]
forall a b. (a, b) -> a
fst ([a], a)
t [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [([a], a) -> a
forall a b. (a, b) -> b
snd ([a], a)
t]
mkInjOp _ _ = String
-> ((FuncMap, IdTypeSPIdMap),
    (SPIdentifier, ([SPIdentifier], SPIdentifier)))
forall a. (?callStack::CallStack) => String -> a
error "SuleCFOL2SoftFOL.mkInjOp: Wrong constructor!!"

mkInjSentences :: IdTypeSPIdMap
               -> FuncMap
               -> [Named SPTerm]
mkInjSentences :: IdTypeSPIdMap -> FuncMap -> [Named SPTerm]
mkInjSentences idMap :: IdTypeSPIdMap
idMap = (SPIdentifier
 -> Set ([SPIdentifier], SPIdentifier)
 -> [Named SPTerm]
 -> [Named SPTerm])
-> [Named SPTerm] -> FuncMap -> [Named SPTerm]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey SPIdentifier
-> Set ([SPIdentifier], SPIdentifier)
-> [Named SPTerm]
-> [Named SPTerm]
forall a.
Show a =>
SPIdentifier
-> Set ([SPIdentifier], a) -> [Named SPTerm] -> [Named SPTerm]
genInjs []
    where genInjs :: SPIdentifier
-> Set ([SPIdentifier], a) -> [Named SPTerm] -> [Named SPTerm]
genInjs k :: SPIdentifier
k tset :: Set ([SPIdentifier], a)
tset fs :: [Named SPTerm]
fs = (([SPIdentifier], a) -> [Named SPTerm] -> [Named SPTerm])
-> [Named SPTerm] -> Set ([SPIdentifier], a) -> [Named SPTerm]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (SPIdentifier
-> ([SPIdentifier], a) -> [Named SPTerm] -> [Named SPTerm]
forall a.
Show a =>
SPIdentifier
-> ([SPIdentifier], a) -> [Named SPTerm] -> [Named SPTerm]
genInj SPIdentifier
k) [Named SPTerm]
fs Set ([SPIdentifier], a)
tset
          genInj :: SPIdentifier
-> ([SPIdentifier], a) -> [Named SPTerm] -> [Named SPTerm]
genInj k :: SPIdentifier
k (args :: [SPIdentifier]
args, res :: a
res) =
              Bool -> [Named SPTerm] -> [Named SPTerm]
forall a. (?callStack::CallStack) => Bool -> a -> a
assert ([SPIdentifier] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SPIdentifier]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1)
                     ([Named SPTerm] -> [Named SPTerm])
-> ([Named SPTerm] -> [Named SPTerm])
-> [Named SPTerm]
-> [Named SPTerm]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> SPTerm -> Named SPTerm
forall a s. a -> s -> SenAttr s a
makeNamed (String -> String -> ShowS
newName (SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
k) (SPIdentifier -> String
forall a. Show a => a -> String
show (SPIdentifier -> String) -> SPIdentifier -> String
forall a b. (a -> b) -> a -> b
$ [SPIdentifier] -> SPIdentifier
forall a. [a] -> a
head [SPIdentifier]
args)
                                 ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
res)
                       (SPQuantSym -> [SPTerm] -> SPTerm -> SPTerm
SPQuantTerm SPQuantSym
SPForall
                              [SPIdentifier -> SPIdentifier -> SPTerm
typedVarTerm SPIdentifier
var (SPIdentifier -> SPTerm) -> SPIdentifier -> SPTerm
forall a b. (a -> b) -> a -> b
$ [SPIdentifier] -> SPIdentifier
forall a. [a] -> a
head [SPIdentifier]
args]
                             (SPSymbol -> [SPTerm] -> SPTerm
compTerm SPSymbol
SPEqual
                                       [SPSymbol -> [SPTerm] -> SPTerm
compTerm (SPIdentifier -> SPSymbol
spSym SPIdentifier
k)
                                                 [SPSymbol -> SPTerm
simpTerm (SPIdentifier -> SPSymbol
spSym SPIdentifier
var)],
                                        SPSymbol -> SPTerm
simpTerm (SPIdentifier -> SPSymbol
spSym SPIdentifier
var)])) Named SPTerm -> [Named SPTerm] -> [Named SPTerm]
forall a. a -> [a] -> [a]
:)
          var :: SPIdentifier
var = String -> SPIdentifier
mkSimpleId (String -> SPIdentifier) -> String -> SPIdentifier
forall a b. (a -> b) -> a -> b
$
            Maybe String -> String
forall a. (?callStack::CallStack) => Maybe a -> a
fromJust ((String -> Bool) -> [String] -> Maybe String
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\ x :: String
x -> Bool -> Bool
not (SPIdentifier -> Set SPIdentifier -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (String -> SPIdentifier
mkSimpleId String
x) Set SPIdentifier
usedIds))
                          ("Y" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [ 'Y' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
i | Int
i <- [(1 :: Int) ..]]))
          newName :: String -> String -> ShowS
newName o :: String
o a :: String
a r :: String
r = "ga_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
o String -> ShowS
forall a. [a] -> [a] -> [a]
++ '_' Char -> ShowS
forall a. a -> [a] -> [a]
: String
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ '_' Char -> ShowS
forall a. a -> [a] -> [a]
: String
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_id"
          usedIds :: Set SPIdentifier
usedIds = IdTypeSPIdMap -> Set SPIdentifier
elemsSPIdSet IdTypeSPIdMap
idMap

{- |
  Translate a CASL signature into SoftFOL signature 'SoftFOL.Sign.Sign'.
  Before translating, eqPredicate symbols where removed from signature.
-}
transSign :: CSign.Sign f e -> (SPSign.Sign, IdTypeSPIdMap)
transSign :: Sign f e -> (Sign, IdTypeSPIdMap)
transSign sign :: Sign f e
sign = (Sign
SPSign.emptySign { sortRel :: Rel SPIdentifier
SPSign.sortRel =
                                 (Id -> SPIdentifier) -> Rel Id -> Rel SPIdentifier
forall a b. (Ord a, Ord b) => (a -> b) -> Rel a -> Rel b
Rel.map Id -> SPIdentifier
transIdSort (Sign f e -> Rel Id
forall f e. Sign f e -> Rel Id
CSign.sortRel Sign f e
sign)
                           , sortMap :: SortMap
sortMap = SortMap
forall a. Map SPIdentifier (Maybe a)
spSortMap
                           , funcMap :: FuncMap
funcMap = FuncMap
fMap
                           , predMap :: PredMap
SPSign.predMap = PredMap
pMap
                           , singleSorted :: Bool
singleSorted = Sign f e -> Bool
forall f e. Sign f e -> Bool
isSingleSorted Sign f e
sign
                           }
                 , IdTypeSPIdMap
idMap'')
    where (spSortMap :: Map SPIdentifier (Maybe a)
spSortMap, idMap :: IdTypeSPIdMap
idMap) =
            (Id
 -> (Map SPIdentifier (Maybe a), IdTypeSPIdMap)
 -> (Map SPIdentifier (Maybe a), IdTypeSPIdMap))
-> (Map SPIdentifier (Maybe a), IdTypeSPIdMap)
-> Set Id
-> (Map SPIdentifier (Maybe a), IdTypeSPIdMap)
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ i :: Id
i (sm :: Map SPIdentifier (Maybe a)
sm, im :: IdTypeSPIdMap
im) ->
                          let sid :: SPIdentifier
sid = CKType
-> SPIdentifier
-> [SPIdentifier]
-> Set SPIdentifier
-> SPIdentifier
disSPOId CKType
CKSort (Id -> SPIdentifier
transIdSort Id
i)
                                       [String -> SPIdentifier
mkSimpleId (String -> SPIdentifier) -> String -> SPIdentifier
forall a b. (a -> b) -> a -> b
$ Int -> ShowS
forall a. Int -> [a] -> [a]
take 20 (ShowS
forall a. [a] -> [a]
cycle "So")]
                                       (Map SPIdentifier (Maybe a) -> Set SPIdentifier
forall k a. Map k a -> Set k
Map.keysSet Map SPIdentifier (Maybe a)
sm)
                          in (SPIdentifier
-> Maybe a
-> Map SPIdentifier (Maybe a)
-> Map SPIdentifier (Maybe a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SPIdentifier
sid Maybe a
forall a. Maybe a
Nothing Map SPIdentifier (Maybe a)
sm,
                              Id -> CType -> SPIdentifier -> IdTypeSPIdMap -> IdTypeSPIdMap
insertSPId Id
i CType
CSort SPIdentifier
sid IdTypeSPIdMap
im))
                                        (Map SPIdentifier (Maybe a)
forall k a. Map k a
Map.empty, IdTypeSPIdMap
forall k a. Map k a
Map.empty)
                                        (Sign f e -> Set Id
forall f e. Sign f e -> Set Id
CSign.sortSet Sign f e
sign)
          (fMap :: FuncMap
fMap, idMap' :: IdTypeSPIdMap
idMap') = IdTypeSPIdMap -> Sign f e -> (FuncMap, IdTypeSPIdMap)
forall e f. IdTypeSPIdMap -> Sign e f -> (FuncMap, IdTypeSPIdMap)
transFuncMap IdTypeSPIdMap
idMap Sign f e
sign
          (pMap :: PredMap
pMap, idMap'' :: IdTypeSPIdMap
idMap'') = IdTypeSPIdMap -> Sign f e -> (PredMap, IdTypeSPIdMap)
forall e f. IdTypeSPIdMap -> Sign e f -> (PredMap, IdTypeSPIdMap)
transPredMap IdTypeSPIdMap
idMap' Sign f e
sign

nonEmptySortSens :: CSign.Sign f e -> IdTypeSPIdMap -> SortMap -> [Named SPTerm]
nonEmptySortSens :: Sign f e -> IdTypeSPIdMap -> SortMap -> [Named SPTerm]
nonEmptySortSens sig :: Sign f e
sig idMap :: IdTypeSPIdMap
idMap sm :: SortMap
sm =
  let es :: Set Id
es = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign f e -> Set Id
forall f e. Sign f e -> Set Id
sortSet Sign f e
sig) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set Id
forall f e. Sign f e -> Set Id
emptySortSet Sign f e
sig
  in [ SPIdentifier -> Named SPTerm
extSen SPIdentifier
s | Id
nes <- Set Id -> [Id]
forall a. Set a -> [a]
Set.toList Set Id
es
     , let s :: SPIdentifier
s = SPIdentifier -> Maybe SPIdentifier -> SPIdentifier
forall a. a -> Maybe a -> a
fromMaybe (Id -> SPIdentifier
transIdSort Id
nes) (Maybe SPIdentifier -> SPIdentifier)
-> Maybe SPIdentifier -> SPIdentifier
forall a b. (a -> b) -> a -> b
$ Id -> CType -> IdTypeSPIdMap -> Maybe SPIdentifier
lookupSPId Id
nes CType
CSort IdTypeSPIdMap
idMap
     , SPIdentifier -> Set SPIdentifier -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SPIdentifier
s (Set SPIdentifier -> Bool) -> Set SPIdentifier -> Bool
forall a b. (a -> b) -> a -> b
$ SortMap -> Set SPIdentifier
forall k a. Map k a -> Set k
Map.keysSet SortMap
sm ]
    where extSen :: SPIdentifier -> Named SPTerm
extSen s :: SPIdentifier
s = String -> SPTerm -> Named SPTerm
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_non_empty_sort_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
s) (SPTerm -> Named SPTerm) -> SPTerm -> Named SPTerm
forall a b. (a -> b) -> a -> b
$ SPQuantSym -> [SPTerm] -> SPTerm -> SPTerm
SPQuantTerm
                     SPQuantSym
SPExists [SPTerm
varTerm] (SPTerm -> SPTerm) -> SPTerm -> SPTerm
forall a b. (a -> b) -> a -> b
$ SPSymbol -> [SPTerm] -> SPTerm
compTerm (SPIdentifier -> SPSymbol
spSym SPIdentifier
s) [SPTerm
varTerm]
              where varTerm :: SPTerm
varTerm = SPSymbol -> SPTerm
simpTerm (SPSymbol -> SPTerm) -> SPSymbol -> SPTerm
forall a b. (a -> b) -> a -> b
$ SPIdentifier -> SPSymbol
spSym (SPIdentifier -> SPSymbol) -> SPIdentifier -> SPSymbol
forall a b. (a -> b) -> a -> b
$ String -> SPIdentifier
mkSimpleId (String -> SPIdentifier) -> String -> SPIdentifier
forall a b. (a -> b) -> a -> b
$ SPIdentifier -> String
forall a. Show a => a -> String
newVar SPIdentifier
s
          newVar :: a -> String
newVar s :: a
s = Maybe String -> String
forall a. (?callStack::CallStack) => Maybe a -> a
fromJust (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$ (String -> Bool) -> [String] -> Maybe String
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= a -> String
forall a. Show a => a -> String
show a
s)
                          ([String] -> Maybe String) -> [String] -> Maybe String
forall a b. (a -> b) -> a -> b
$ "Y" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: ['Y' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
i | Int
i <- [(1 :: Int) ..]]

disjointTopSorts :: CSign.Sign f e -> IdTypeSPIdMap -> [Named SPTerm]
disjointTopSorts :: Sign f e -> IdTypeSPIdMap -> [Named SPTerm]
disjointTopSorts sign :: Sign f e
sign idMap :: IdTypeSPIdMap
idMap = let
    s :: Set Id
s = Sign f e -> Set Id
forall f e. Sign f e -> Set Id
CSign.sortSet Sign f e
sign
    sl :: [Set Id]
sl = (Id -> Id -> Bool) -> Set Id -> [Set Id]
forall a. Ord a => (a -> a -> Bool) -> Set a -> [Set a]
Rel.partSet (Bool -> Sign f e -> Id -> Id -> Bool
forall f e. Bool -> Sign f e -> Id -> Id -> Bool
haveCommonSupersorts Bool
True Sign f e
sign) Set Id
s
    l :: [Id]
l = (Set Id -> Id) -> [Set Id] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map (\ p :: Set Id
p -> case Bool -> Sign f e -> (Id -> Id) -> [Id] -> [Id]
forall f e a. Bool -> Sign f e -> (a -> Id) -> [a] -> [a]
keepMinimals1 Bool
False Sign f e
sign Id -> Id
forall a. a -> a
id ([Id] -> [Id]) -> [Id] -> [Id]
forall a b. (a -> b) -> a -> b
$ Set Id -> [Id]
forall a. Set a -> [a]
Set.toList Set Id
p of
                       [e :: Id
e] -> Id
e
                       _ -> String -> Id
forall a. (?callStack::CallStack) => String -> a
error "disjointTopSorts") [Set Id]
sl
    pairs :: [b] -> [(b, b)]
pairs ls :: [b]
ls = case [b]
ls of
      s1 :: b
s1 : r :: [b]
r -> (b -> (b, b)) -> [b] -> [(b, b)]
forall a b. (a -> b) -> [a] -> [b]
map (\ s2 :: b
s2 -> (b
s1, b
s2)) [b]
r [(b, b)] -> [(b, b)] -> [(b, b)]
forall a. [a] -> [a] -> [a]
++ [b] -> [(b, b)]
pairs [b]
r
      _ -> []
    v1 :: SPTerm
v1 = SPSymbol -> SPTerm
simpTerm (SPSymbol -> SPTerm) -> SPSymbol -> SPTerm
forall a b. (a -> b) -> a -> b
$ SPIdentifier -> SPSymbol
spSym (SPIdentifier -> SPSymbol) -> SPIdentifier -> SPSymbol
forall a b. (a -> b) -> a -> b
$ String -> SPIdentifier
mkSimpleId "Y1"
    v2 :: SPTerm
v2 = SPSymbol -> SPTerm
simpTerm (SPSymbol -> SPTerm) -> SPSymbol -> SPTerm
forall a b. (a -> b) -> a -> b
$ SPIdentifier -> SPSymbol
spSym (SPIdentifier -> SPSymbol) -> SPIdentifier -> SPSymbol
forall a b. (a -> b) -> a -> b
$ String -> SPIdentifier
mkSimpleId "Y2"
    in ((SPIdentifier, SPIdentifier) -> Named SPTerm)
-> [(SPIdentifier, SPIdentifier)] -> [Named SPTerm]
forall a b. (a -> b) -> [a] -> [b]
map (\ (t1 :: SPIdentifier
t1, t2 :: SPIdentifier
t2) ->
         String -> SPTerm -> Named SPTerm
forall a s. a -> s -> SenAttr s a
makeNamed ("disjoint_sorts_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPIdentifier -> ShowS
forall a. Show a => a -> ShowS
shows SPIdentifier
t1 "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
t2) (SPTerm -> Named SPTerm) -> SPTerm -> Named SPTerm
forall a b. (a -> b) -> a -> b
$
           SPQuantSym -> [SPTerm] -> SPTerm -> SPTerm
SPQuantTerm SPQuantSym
SPForall
               [ SPSymbol -> [SPTerm] -> SPTerm
compTerm (SPIdentifier -> SPSymbol
spSym SPIdentifier
t1) [SPTerm
v1]
               , SPSymbol -> [SPTerm] -> SPTerm
compTerm (SPIdentifier -> SPSymbol
spSym SPIdentifier
t2) [SPTerm
v2]]
              (SPTerm -> SPTerm) -> SPTerm -> SPTerm
forall a b. (a -> b) -> a -> b
$ SPSymbol -> [SPTerm] -> SPTerm
compTerm SPSymbol
SPNot [SPTerm -> SPTerm -> SPTerm
mkEq SPTerm
v1 SPTerm
v2]) ([(SPIdentifier, SPIdentifier)] -> [Named SPTerm])
-> [(SPIdentifier, SPIdentifier)] -> [Named SPTerm]
forall a b. (a -> b) -> a -> b
$ [SPIdentifier] -> [(SPIdentifier, SPIdentifier)]
forall b. [b] -> [(b, b)]
pairs ([SPIdentifier] -> [(SPIdentifier, SPIdentifier)])
-> [SPIdentifier] -> [(SPIdentifier, SPIdentifier)]
forall a b. (a -> b) -> a -> b
$
                (Id -> SPIdentifier) -> [Id] -> [SPIdentifier]
forall a b. (a -> b) -> [a] -> [b]
map (\ t :: Id
t -> SPIdentifier -> Maybe SPIdentifier -> SPIdentifier
forall a. a -> Maybe a -> a
fromMaybe (Id -> SPIdentifier
transIdSort Id
t)
                     (Maybe SPIdentifier -> SPIdentifier)
-> Maybe SPIdentifier -> SPIdentifier
forall a b. (a -> b) -> a -> b
$ Id -> CType -> IdTypeSPIdMap -> Maybe SPIdentifier
lookupSPId Id
t CType
CSort IdTypeSPIdMap
idMap) [Id]
l

transTheory :: (FormExtension f, Eq f) =>
               SignTranslator f e
            -> FormulaTranslator f e
            -> (CSign.Sign f e, [Named (FORMULA f)])
            -> Result SoftFOLTheory
transTheory :: SignTranslator f e
-> FormulaTranslator f e
-> (Sign f e, [Named (FORMULA f)])
-> Result SoftFOLTheory
transTheory trSig :: SignTranslator f e
trSig trForm :: FormulaTranslator f e
trForm (sign :: Sign f e
sign, sens :: [Named (FORMULA f)]
sens) =
  let (nsig :: Sign f e
nsig, sm :: Sort_map
sm) = Sign f e -> (Sign f e, Sort_map)
forall f e. Sign f e -> (Sign f e, Sort_map)
removeSortCycles Sign f e
sign
  in SignTranslator f e
-> FormulaTranslator f e
-> (Sign f e, [Named (FORMULA f)])
-> Result SoftFOLTheory
forall f e.
(FormExtension f, Eq f) =>
SignTranslator f e
-> FormulaTranslator f e
-> (Sign f e, [Named (FORMULA f)])
-> Result SoftFOLTheory
transTheoryAux SignTranslator f e
trSig FormulaTranslator f e
trForm (Sign f e
nsig
     , (Named (FORMULA f) -> Named (FORMULA f))
-> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA f -> FORMULA f) -> Named (FORMULA f) -> Named (FORMULA f)
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed ((FORMULA f -> FORMULA f)
 -> Named (FORMULA f) -> Named (FORMULA f))
-> (FORMULA f -> FORMULA f)
-> Named (FORMULA f)
-> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ MapSen f e () -> Morphism f e () -> FORMULA f -> FORMULA f
forall f e m.
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapMorphForm ((f -> f) -> MapSen f e ()
forall (m :: * -> *) a. Monad m => a -> m a
return f -> f
forall a. a -> a
id)
                 ((() -> Sign f e -> Sign f e -> Morphism f e ()
forall m f e. m -> Sign f e -> Sign f e -> Morphism f e m
embedMorphism () Sign f e
sign Sign f e
nsig) { sort_map :: Sort_map
sort_map = Sort_map
sm })) [Named (FORMULA f)]
sens)

transTheoryAux :: (FormExtension f, Eq f) =>
               SignTranslator f e
            -> FormulaTranslator f e
            -> (CSign.Sign f e, [Named (FORMULA f)])
            -> Result SoftFOLTheory
transTheoryAux :: SignTranslator f e
-> FormulaTranslator f e
-> (Sign f e, [Named (FORMULA f)])
-> Result SoftFOLTheory
transTheoryAux trSig :: SignTranslator f e
trSig trForm :: FormulaTranslator f e
trForm (sign :: Sign f e
sign, sens :: [Named (FORMULA f)]
sens) =
  (SoftFOLTheory -> SoftFOLTheory)
-> Result SoftFOLTheory -> Result SoftFOLTheory
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SignTranslator f e
trSig Sign f e
sign (Sign f e -> e
forall f e. Sign f e -> e
CSign.extendedInfo Sign f e
sign))
    (case Sign f e -> (Sign, IdTypeSPIdMap)
forall f e. Sign f e -> (Sign, IdTypeSPIdMap)
transSign (Sign f e -> Sign f e
forall f e. Sign f e -> Sign f e
filterPreds (Sign f e -> Sign f e) -> Sign f e -> Sign f e
forall a b. (a -> b) -> a -> b
$ (Sign f e -> Named (FORMULA f) -> Sign f e)
-> Sign f e -> [Named (FORMULA f)] -> Sign f e
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Sign f e -> Named (FORMULA f) -> Sign f e
forall f e f a. Sign f e -> SenAttr (FORMULA f) a -> Sign f e
insInjOps Sign f e
sign [Named (FORMULA f)]
genAxs) of
     (tSign :: Sign
tSign, idMap :: IdTypeSPIdMap
idMap) ->
        do (idMap' :: IdTypeSPIdMap
idMap', tSign' :: Sign
tSign', sentencesAndGoals :: [Named SPTerm]
sentencesAndGoals) <-
               IdTypeSPIdMap
-> [Named (FORMULA f)]
-> Sign
-> Result (IdTypeSPIdMap, Sign, [Named SPTerm])
forall f.
IdTypeSPIdMap
-> [Named (FORMULA f)]
-> Sign
-> Result (IdTypeSPIdMap, Sign, [Named SPTerm])
integrateGenerated IdTypeSPIdMap
idMap [Named (FORMULA f)]
genSens Sign
tSign
           let tSignElim :: Sign
tSignElim = if Sign -> Bool
SPSign.singleSortNotGen Sign
tSign'
                             then Sign
tSign' {sortMap :: SortMap
sortMap = SortMap
forall k a. Map k a
Map.empty} else Sign
tSign'
           SoftFOLTheory -> Result SoftFOLTheory
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
tSignElim,
                    Sign f e -> IdTypeSPIdMap -> [Named SPTerm]
forall f e. Sign f e -> IdTypeSPIdMap -> [Named SPTerm]
disjointTopSorts Sign f e
sign IdTypeSPIdMap
idMap' [Named SPTerm] -> [Named SPTerm] -> [Named SPTerm]
forall a. [a] -> [a] -> [a]
++
                    [Named SPTerm]
sentencesAndGoals [Named SPTerm] -> [Named SPTerm] -> [Named SPTerm]
forall a. [a] -> [a] -> [a]
++
                    Sign f e -> IdTypeSPIdMap -> SortMap -> [Named SPTerm]
forall f e. Sign f e -> IdTypeSPIdMap -> SortMap -> [Named SPTerm]
nonEmptySortSens Sign f e
sign IdTypeSPIdMap
idMap' (Sign -> SortMap
sortMap Sign
tSignElim) [Named SPTerm] -> [Named SPTerm] -> [Named SPTerm]
forall a. [a] -> [a] -> [a]
++
                    (Named (FORMULA f) -> Named SPTerm)
-> [Named (FORMULA f)] -> [Named SPTerm]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA f -> SPTerm) -> Named (FORMULA f) -> Named SPTerm
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed (Bool
-> Set PRED_SYMB
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> FORMULA f
-> SPTerm
forall f e.
(Eq f, FormExtension f) =>
Bool
-> Set PRED_SYMB
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> FORMULA f
-> SPTerm
transFORM (Sign -> Bool
singleSortNotGen Sign
tSign') Set PRED_SYMB
eqPreds
                                     Sign f e
sign IdTypeSPIdMap
idMap' FormulaTranslator f e
trForm))
                        [Named (FORMULA f)]
realSens'))

  where (genSens :: [Named (FORMULA f)]
genSens, realSens :: [Named (FORMULA f)]
realSens) =
            (Named (FORMULA f) -> Bool)
-> [Named (FORMULA f)]
-> ([Named (FORMULA f)], [Named (FORMULA f)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\ s :: Named (FORMULA f)
s -> case Named (FORMULA f) -> FORMULA f
forall s a. SenAttr s a -> s
sentence Named (FORMULA f)
s of
                              Sort_gen_ax _ _ -> Bool
True
                              _ -> Bool
False) [Named (FORMULA f)]
sens
        (eqPreds :: Set PRED_SYMB
eqPreds, realSens' :: [Named (FORMULA f)]
realSens') = ((Set PRED_SYMB, [Named (FORMULA f)])
 -> Named (FORMULA f) -> (Set PRED_SYMB, [Named (FORMULA f)]))
-> (Set PRED_SYMB, [Named (FORMULA f)])
-> [Named (FORMULA f)]
-> (Set PRED_SYMB, [Named (FORMULA f)])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Set PRED_SYMB, [Named (FORMULA f)])
-> Named (FORMULA f) -> (Set PRED_SYMB, [Named (FORMULA f)])
forall f.
Eq f =>
(Set PRED_SYMB, [Named (FORMULA f)])
-> Named (FORMULA f) -> (Set PRED_SYMB, [Named (FORMULA f)])
findEqPredicates (Set PRED_SYMB
forall a. Set a
Set.empty, []) [Named (FORMULA f)]
realSens
        genAxs :: [Named (FORMULA f)]
genAxs = (Named (FORMULA f) -> Bool)
-> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. (a -> Bool) -> [a] -> [a]
filter Named (FORMULA f) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom [Named (FORMULA f)]
genSens
        insInjOps :: Sign f e -> SenAttr (FORMULA f) a -> Sign f e
insInjOps sig :: Sign f e
sig s :: SenAttr (FORMULA f) a
s =
              case SenAttr (FORMULA f) a -> FORMULA f
forall s a. SenAttr s a -> s
sentence SenAttr (FORMULA f) a
s of
              (Sort_gen_ax constrs :: [Constraint]
constrs _) ->
                 case [Constraint] -> ([Id], [OP_SYMB], [(Id, Id)])
recover_Sort_gen_ax [Constraint]
constrs of
                 (_, ops :: [OP_SYMB]
ops, mp :: [(Id, Id)]
mp) -> Bool -> Sign f e -> Sign f e
forall a. (?callStack::CallStack) => Bool -> a -> a
assert ([(Id, Id)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Id, Id)]
mp) (Sign f e -> [OP_SYMB] -> Sign f e
forall f e. Sign f e -> [OP_SYMB] -> Sign f e
insertInjOps Sign f e
sig [OP_SYMB]
ops)
              _ -> String -> Sign f e
forall a. (?callStack::CallStack) => String -> a
error "SuleCFOL2SoftFOL.transTheory.insInjOps"
        filterPreds :: Sign f e -> Sign f e
filterPreds sig :: Sign f e
sig =
              Sign f e
sig { predMap :: MapSet Id PredType
CSign.predMap = MapSet Id PredType -> MapSet Id PredType -> MapSet Id PredType
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.difference
                (Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
CSign.predMap Sign f e
sig)
                ((PRED_SYMB -> MapSet Id PredType -> MapSet Id PredType)
-> MapSet Id PredType -> Set PRED_SYMB -> MapSet Id PredType
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ pl :: PRED_SYMB
pl -> case PRED_SYMB
pl of
                      Pred_name pn :: Id
pn -> Id -> PredType -> MapSet Id PredType -> MapSet Id PredType
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert Id
pn ([Id] -> PredType
PredType [])
                      Qual_pred_name pn :: Id
pn pt :: PRED_TYPE
pt _ ->
                        Id -> PredType -> MapSet Id PredType -> MapSet Id PredType
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert Id
pn (PredType -> MapSet Id PredType -> MapSet Id PredType)
-> PredType -> MapSet Id PredType -> MapSet Id PredType
forall a b. (a -> b) -> a -> b
$ PRED_TYPE -> PredType
CSign.toPredType PRED_TYPE
pt)
                    MapSet Id PredType
forall a b. MapSet a b
MapSet.empty Set PRED_SYMB
eqPreds) }

{- |
 Finds definitions (Equivalences) where one side is a binary predicate
 and the other side is a built-in equality application (Strong_equation).
 The given Named (FORMULA f) is checked for this and if so, will be put
 into the set of such predicates.
-}
findEqPredicates :: (Eq f) => (Set.Set PRED_SYMB, [Named (FORMULA f)])
                    -- ^ previous list of found predicates and valid sentences
                 -> Named (FORMULA f)
                    -- ^ sentence to check
                 -> (Set.Set PRED_SYMB, [Named (FORMULA f)])
findEqPredicates :: (Set PRED_SYMB, [Named (FORMULA f)])
-> Named (FORMULA f) -> (Set PRED_SYMB, [Named (FORMULA f)])
findEqPredicates (eqPreds :: Set PRED_SYMB
eqPreds, sens :: [Named (FORMULA f)]
sens) sen :: Named (FORMULA f)
sen =
    case Named (FORMULA f) -> FORMULA f
forall s a. SenAttr s a -> s
sentence Named (FORMULA f)
sen of
      Quantification Universal var_decl :: [VAR_DECL]
var_decl quantFormula :: FORMULA f
quantFormula _ ->
        [(SPIdentifier, Id)]
-> FORMULA f -> (Set PRED_SYMB, [Named (FORMULA f)])
forall f.
[(SPIdentifier, Id)]
-> FORMULA f -> (Set PRED_SYMB, [Named (FORMULA f)])
isEquiv (([(SPIdentifier, Id)] -> VAR_DECL -> [(SPIdentifier, Id)])
-> [(SPIdentifier, Id)] -> [VAR_DECL] -> [(SPIdentifier, Id)]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ vList :: [(SPIdentifier, Id)]
vList (Var_decl v :: [SPIdentifier]
v s :: Id
s _) ->
                          [(SPIdentifier, Id)]
vList [(SPIdentifier, Id)]
-> [(SPIdentifier, Id)] -> [(SPIdentifier, Id)]
forall a. [a] -> [a] -> [a]
++ (SPIdentifier -> (SPIdentifier, Id))
-> [SPIdentifier] -> [(SPIdentifier, Id)]
forall a b. (a -> b) -> [a] -> [b]
map (\ vl :: SPIdentifier
vl -> (SPIdentifier
vl, Id
s)) [SPIdentifier]
v)
                       [] [VAR_DECL]
var_decl)
                FORMULA f
quantFormula
      _ -> (Set PRED_SYMB, [Named (FORMULA f)])
validSens

  where
    validSens :: (Set PRED_SYMB, [Named (FORMULA f)])
validSens = (Set PRED_SYMB
eqPreds, [Named (FORMULA f)]
sens [Named (FORMULA f)] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a] -> [a]
++ [Named (FORMULA f)
sen])
    isEquiv :: [(SPIdentifier, Id)]
-> FORMULA f -> (Set PRED_SYMB, [Named (FORMULA f)])
isEquiv vars :: [(SPIdentifier, Id)]
vars qf :: FORMULA f
qf =
      {- Exact two variables are checked if they have the same Sort.
      If more than two variables should be compared, use foldl. -}
      if ([(SPIdentifier, Id)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(SPIdentifier, Id)]
vars Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 2) Bool -> Bool -> Bool
&& ((SPIdentifier, Id) -> Id
forall a b. (a, b) -> b
snd ([(SPIdentifier, Id)] -> (SPIdentifier, Id)
forall a. [a] -> a
head [(SPIdentifier, Id)]
vars) Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== (SPIdentifier, Id) -> Id
forall a b. (a, b) -> b
snd ([(SPIdentifier, Id)]
vars [(SPIdentifier, Id)] -> Int -> (SPIdentifier, Id)
forall a. [a] -> Int -> a
!! 1))
       then case FORMULA f
qf of
          Relation f1 :: FORMULA f
f1 Equivalence f2 :: FORMULA f
f2 _ -> [(SPIdentifier, Id)]
-> FORMULA f -> FORMULA f -> (Set PRED_SYMB, [Named (FORMULA f)])
forall f.
[(SPIdentifier, Id)]
-> FORMULA f -> FORMULA f -> (Set PRED_SYMB, [Named (FORMULA f)])
isStrong_eq [(SPIdentifier, Id)]
vars FORMULA f
f1 FORMULA f
f2
          _ -> (Set PRED_SYMB, [Named (FORMULA f)])
validSens
        else (Set PRED_SYMB, [Named (FORMULA f)])
validSens
    isStrong_eq :: [(SPIdentifier, Id)]
-> FORMULA f -> FORMULA f -> (Set PRED_SYMB, [Named (FORMULA f)])
isStrong_eq vars :: [(SPIdentifier, Id)]
vars f1 :: FORMULA f
f1 f2 :: FORMULA f
f2 =
      let f1n :: FORMULA f
f1n = case FORMULA f
f1 of
                  Equation _ Strong _ _ -> FORMULA f
f1
                  _ -> FORMULA f
f2
          f2n :: FORMULA f
f2n = case FORMULA f
f1 of
                  Equation _ Strong _ _ -> FORMULA f
f2
                  _ -> FORMULA f
f1
      in case FORMULA f
f1n of
            Equation eq_t1 :: TERM f
eq_t1 Strong eq_t2 :: TERM f
eq_t2 _ -> case FORMULA f
f2n of
              Predication eq_pred_symb :: PRED_SYMB
eq_pred_symb pterms :: [TERM f]
pterms _ ->
                if Map SPIdentifier Id -> [(SPIdentifier, Id)]
forall k a. Map k a -> [(k, a)]
Map.toList ([(SPIdentifier, Id)] -> Map SPIdentifier Id
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(SPIdentifier, Id)] -> Map SPIdentifier Id)
-> [(SPIdentifier, Id)] -> Map SPIdentifier Id
forall a b. (a -> b) -> a -> b
$ [TERM f] -> [(SPIdentifier, Id)]
forall f. [TERM f] -> [(SPIdentifier, Id)]
sortedVarTermList [TERM f]
pterms)
                     [(SPIdentifier, Id)] -> [(SPIdentifier, Id)] -> Bool
forall a. Eq a => a -> a -> Bool
== Map SPIdentifier Id -> [(SPIdentifier, Id)]
forall k a. Map k a -> [(k, a)]
Map.toList ([(SPIdentifier, Id)] -> Map SPIdentifier Id
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(SPIdentifier, Id)]
vars)
                 Bool -> Bool -> Bool
&& Map SPIdentifier Id -> [(SPIdentifier, Id)]
forall k a. Map k a -> [(k, a)]
Map.toList
                         ([(SPIdentifier, Id)] -> Map SPIdentifier Id
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(SPIdentifier, Id)] -> Map SPIdentifier Id)
-> [(SPIdentifier, Id)] -> Map SPIdentifier Id
forall a b. (a -> b) -> a -> b
$ [TERM f] -> [(SPIdentifier, Id)]
forall f. [TERM f] -> [(SPIdentifier, Id)]
sortedVarTermList [TERM f
eq_t1, TERM f
eq_t2])
                     [(SPIdentifier, Id)] -> [(SPIdentifier, Id)] -> Bool
forall a. Eq a => a -> a -> Bool
== Map SPIdentifier Id -> [(SPIdentifier, Id)]
forall k a. Map k a -> [(k, a)]
Map.toList ([(SPIdentifier, Id)] -> Map SPIdentifier Id
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(SPIdentifier, Id)]
vars)
                  then (PRED_SYMB -> Set PRED_SYMB -> Set PRED_SYMB
forall a. Ord a => a -> Set a -> Set a
Set.insert PRED_SYMB
eq_pred_symb Set PRED_SYMB
eqPreds, [Named (FORMULA f)]
sens)
                  else (Set PRED_SYMB, [Named (FORMULA f)])
validSens
              _ -> (Set PRED_SYMB, [Named (FORMULA f)])
validSens
            _ -> (Set PRED_SYMB, [Named (FORMULA f)])
validSens

{- |
  Creates a list of (VAR, SORT) out of a list of TERMs. Only Qual_var TERMs
  are inserted which will be checked using
  'Comorphisms.SuleCFOL2SoftFOL.hasSortedVarTerm'.
-}
sortedVarTermList :: [TERM f] -> [(VAR, SORT)]
sortedVarTermList :: [TERM f] -> [(SPIdentifier, Id)]
sortedVarTermList = (TERM f -> Maybe (SPIdentifier, Id))
-> [TERM f] -> [(SPIdentifier, Id)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TERM f -> Maybe (SPIdentifier, Id)
forall f. TERM f -> Maybe (SPIdentifier, Id)
hasSortedVarTerm

{- |
  Finds a 'CASL.AS_Basic_CASL.Qual_var' term recursively if super term(s) is
  'CASL.AS_Basic_CASL.Sorted_term' or 'CASL.AS_Basic_CASL.Cast'.
-}
hasSortedVarTerm :: TERM f -> Maybe (VAR, SORT)
hasSortedVarTerm :: TERM f -> Maybe (SPIdentifier, Id)
hasSortedVarTerm t :: TERM f
t = case TERM f
t of
    Qual_var v :: SPIdentifier
v s :: Id
s _ -> (SPIdentifier, Id) -> Maybe (SPIdentifier, Id)
forall a. a -> Maybe a
Just (SPIdentifier
v, Id
s)
    Sorted_term tx :: TERM f
tx _ _ -> TERM f -> Maybe (SPIdentifier, Id)
forall f. TERM f -> Maybe (SPIdentifier, Id)
hasSortedVarTerm TERM f
tx
    Cast tx :: TERM f
tx _ _ -> TERM f -> Maybe (SPIdentifier, Id)
forall f. TERM f -> Maybe (SPIdentifier, Id)
hasSortedVarTerm TERM f
tx
    _ -> Maybe (SPIdentifier, Id)
forall a. Maybe a
Nothing


-- ---------------------------- Formulas ------------------------------

transOPSYMB :: IdTypeSPIdMap -> OP_SYMB -> SPIdentifier
transOPSYMB :: IdTypeSPIdMap -> OP_SYMB -> SPIdentifier
transOPSYMB idMap :: IdTypeSPIdMap
idMap ~qo :: OP_SYMB
qo@(Qual_op_name op :: Id
op ot :: OP_TYPE
ot _) =
    SPIdentifier -> Maybe SPIdentifier -> SPIdentifier
forall a. a -> Maybe a -> a
fromMaybe (String -> SPIdentifier
forall a. (?callStack::CallStack) => String -> a
error (String -> SPIdentifier) -> String -> SPIdentifier
forall a b. (a -> b) -> a -> b
$ "SuleCFOL2SoftFOL.transOPSYMB: unknown op: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ OP_SYMB -> String
forall a. Show a => a -> String
show OP_SYMB
qo)
        (Id -> CType -> IdTypeSPIdMap -> Maybe SPIdentifier
lookupSPId Id
op (OpType -> CType
COp (OP_TYPE -> OpType
CSign.toOpType OP_TYPE
ot)) IdTypeSPIdMap
idMap)

transPREDSYMB :: IdTypeSPIdMap -> PRED_SYMB -> SPIdentifier
transPREDSYMB :: IdTypeSPIdMap -> PRED_SYMB -> SPIdentifier
transPREDSYMB idMap :: IdTypeSPIdMap
idMap ~qp :: PRED_SYMB
qp@(Qual_pred_name p :: Id
p pt :: PRED_TYPE
pt _) = SPIdentifier -> Maybe SPIdentifier -> SPIdentifier
forall a. a -> Maybe a -> a
fromMaybe
    (String -> SPIdentifier
forall a. (?callStack::CallStack) => String -> a
error (String -> SPIdentifier) -> String -> SPIdentifier
forall a b. (a -> b) -> a -> b
$ "SuleCFOL2SoftFOL.transPREDSYMB: unknown pred: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ PRED_SYMB -> String
forall a. Show a => a -> String
show PRED_SYMB
qp)
          (Id -> CType -> IdTypeSPIdMap -> Maybe SPIdentifier
lookupSPId Id
p (PredType -> CType
CPred (PRED_TYPE -> PredType
CSign.toPredType PRED_TYPE
pt)) IdTypeSPIdMap
idMap)

-- | Translate the quantifier
quantify :: QUANTIFIER -> SPQuantSym
quantify :: QUANTIFIER -> SPQuantSym
quantify q :: QUANTIFIER
q = case QUANTIFIER
q of
    Universal -> SPQuantSym
SPForall
    Existential -> SPQuantSym
SPExists
    Unique_existential ->
      String -> SPQuantSym
forall a. (?callStack::CallStack) => String -> a
error "SuleCFOL2SoftFOL: no translation for existential quantification."

transVarTup :: (Set.Set SPIdentifier, IdTypeSPIdMap) ->
               (VAR, SORT) ->
               ((Set.Set SPIdentifier, IdTypeSPIdMap),
                (SPIdentifier, SPIdentifier))
                {- ^ ((new set of used Ids, new map of Ids to original Ids),
                (var as sp_Id, sort as sp_Id)) -}
transVarTup :: (Set SPIdentifier, IdTypeSPIdMap)
-> (SPIdentifier, Id)
-> ((Set SPIdentifier, IdTypeSPIdMap),
    (SPIdentifier, SPIdentifier))
transVarTup (usedIds :: Set SPIdentifier
usedIds, idMap :: IdTypeSPIdMap
idMap) (v :: SPIdentifier
v, s :: Id
s) =
    ((SPIdentifier -> Set SPIdentifier -> Set SPIdentifier
forall a. Ord a => a -> Set a -> Set a
Set.insert SPIdentifier
sid Set SPIdentifier
usedIds,
      Id -> CType -> SPIdentifier -> IdTypeSPIdMap -> IdTypeSPIdMap
insertSPId Id
vi (Id -> CType
CVar Id
s) SPIdentifier
sid (IdTypeSPIdMap -> IdTypeSPIdMap) -> IdTypeSPIdMap -> IdTypeSPIdMap
forall a b. (a -> b) -> a -> b
$ Id -> CType -> IdTypeSPIdMap -> IdTypeSPIdMap
deleteSPId Id
vi (Id -> CType
CVar Id
s) IdTypeSPIdMap
idMap)
    , (SPIdentifier
sid, SPIdentifier
spSort))
    where spSort :: SPIdentifier
spSort = SPIdentifier -> Maybe SPIdentifier -> SPIdentifier
forall a. a -> Maybe a -> a
fromMaybe
            (String -> SPIdentifier
forall a. (?callStack::CallStack) => String -> a
error (String -> SPIdentifier) -> String -> SPIdentifier
forall a b. (a -> b) -> a -> b
$ "SuleCFOL2SoftFOL: translation of sort \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++
             Id -> ShowS
forall a. Pretty a => a -> ShowS
showDoc Id
s "\" not found")
            (Id -> CType -> IdTypeSPIdMap -> Maybe SPIdentifier
lookupSPId Id
s CType
CSort IdTypeSPIdMap
idMap)
          vi :: Id
vi = SPIdentifier -> Id
simpleIdToId SPIdentifier
v
          sid :: SPIdentifier
sid = CKType
-> SPIdentifier
-> [SPIdentifier]
-> Set SPIdentifier
-> SPIdentifier
disSPOId CKType
CKVar (CKType -> Id -> SPIdentifier
transId CKType
CKVar Id
vi)
                    [String -> SPIdentifier
mkSimpleId (String -> SPIdentifier) -> String -> SPIdentifier
forall a b. (a -> b) -> a -> b
$ "_Va_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> ShowS
forall a. Pretty a => a -> ShowS
showDoc Id
s "_Va"]
                    Set SPIdentifier
usedIds

transFORM :: (Eq f, FormExtension f) => Bool -- ^ single sorted flag
          -> Set.Set PRED_SYMB -- ^ list of predicates to substitute
          -> CSign.Sign f e
          -> IdTypeSPIdMap -> FormulaTranslator f e
          -> FORMULA f -> SPTerm
transFORM :: Bool
-> Set PRED_SYMB
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> FORMULA f
-> SPTerm
transFORM siSo :: Bool
siSo eqPreds :: Set PRED_SYMB
eqPreds sign :: Sign f e
sign i :: IdTypeSPIdMap
i tr :: FormulaTranslator f e
tr phi :: FORMULA f
phi = Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> FORMULA f
-> SPTerm
forall f e.
FormExtension f =>
Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> FORMULA f
-> SPTerm
transFORMULA Bool
siSo Sign f e
sign IdTypeSPIdMap
i FormulaTranslator f e
tr FORMULA f
phi'
    where phi' :: FORMULA f
phi' = (f -> f) -> FORMULA f -> FORMULA f
forall f. Eq f => (f -> f) -> FORMULA f -> FORMULA f
codeOutConditionalF f -> f
forall a. a -> a
id
                     ((f -> f) -> (f -> f) -> FORMULA f -> FORMULA f
forall f. (f -> f) -> (f -> f) -> FORMULA f -> FORMULA f
codeOutUniqueExtF f -> f
forall a. a -> a
id f -> f
forall a. a -> a
id
                          (Set PRED_SYMB -> (f -> f) -> FORMULA f -> FORMULA f
forall f. Set PRED_SYMB -> (f -> f) -> FORMULA f -> FORMULA f
substEqPreds Set PRED_SYMB
eqPreds f -> f
forall a. a -> a
id FORMULA f
phi))


transFORMULA :: FormExtension f => Bool -> CSign.Sign f e -> IdTypeSPIdMap
             -> FormulaTranslator f e -> FORMULA f -> SPTerm
transFORMULA :: Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> FORMULA f
-> SPTerm
transFORMULA siSo :: Bool
siSo sign :: Sign f e
sign idMap :: IdTypeSPIdMap
idMap tr :: FormulaTranslator f e
tr frm :: FORMULA f
frm = case FORMULA f
frm of
  Quantification qu :: QUANTIFIER
qu vdecl :: [VAR_DECL]
vdecl phi :: FORMULA f
phi _ ->
    SPQuantSym -> [SPTerm] -> SPTerm -> SPTerm
SPQuantTerm (QUANTIFIER -> SPQuantSym
quantify QUANTIFIER
qu)
                    [SPTerm]
vList
                    (Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> FORMULA f
-> SPTerm
forall f e.
FormExtension f =>
Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> FORMULA f
-> SPTerm
transFORMULA Bool
siSo Sign f e
sign IdTypeSPIdMap
idMap' FormulaTranslator f e
tr FORMULA f
phi)
    where ((_, idMap' :: IdTypeSPIdMap
idMap'), vList :: [SPTerm]
vList) =
              ((Set SPIdentifier, IdTypeSPIdMap)
 -> (SPIdentifier, Id)
 -> ((Set SPIdentifier, IdTypeSPIdMap), SPTerm))
-> (Set SPIdentifier, IdTypeSPIdMap)
-> [(SPIdentifier, Id)]
-> ((Set SPIdentifier, IdTypeSPIdMap), [SPTerm])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL (\ acc :: (Set SPIdentifier, IdTypeSPIdMap)
acc e :: (SPIdentifier, Id)
e ->
                  let (acc' :: (Set SPIdentifier, IdTypeSPIdMap)
acc', e' :: (SPIdentifier, SPIdentifier)
e') = (Set SPIdentifier, IdTypeSPIdMap)
-> (SPIdentifier, Id)
-> ((Set SPIdentifier, IdTypeSPIdMap),
    (SPIdentifier, SPIdentifier))
transVarTup (Set SPIdentifier, IdTypeSPIdMap)
acc (SPIdentifier, Id)
e
                  in ((Set SPIdentifier, IdTypeSPIdMap)
acc', (if Bool
siSo then SPSymbol -> SPTerm
simpTerm (SPSymbol -> SPTerm)
-> ((SPIdentifier, SPIdentifier) -> SPSymbol)
-> (SPIdentifier, SPIdentifier)
-> SPTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPIdentifier -> SPSymbol
spSym (SPIdentifier -> SPSymbol)
-> ((SPIdentifier, SPIdentifier) -> SPIdentifier)
-> (SPIdentifier, SPIdentifier)
-> SPSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SPIdentifier, SPIdentifier) -> SPIdentifier
forall a b. (a, b) -> a
fst
                                     else (SPIdentifier -> SPIdentifier -> SPTerm)
-> (SPIdentifier, SPIdentifier) -> SPTerm
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SPIdentifier -> SPIdentifier -> SPTerm
typedVarTerm)
                            (SPIdentifier, SPIdentifier)
e'))
                        (Set SPIdentifier
sidSet, IdTypeSPIdMap
idMap) ([VAR_DECL] -> [(SPIdentifier, Id)]
flatVAR_DECLs [VAR_DECL]
vdecl)
          sidSet :: Set SPIdentifier
sidSet = IdTypeSPIdMap -> Set SPIdentifier
elemsSPIdSet IdTypeSPIdMap
idMap
  Junction j :: Junctor
j phis :: [FORMULA f]
phis _ -> let
    (n :: SPSymbol
n, op :: SPTerm -> SPTerm -> SPTerm
op) = if Junctor
j Junctor -> Junctor -> Bool
forall a. Eq a => a -> a -> Bool
== Junctor
Dis then (SPSymbol
SPFalse, SPTerm -> SPTerm -> SPTerm
mkDisj) else (SPSymbol
SPTrue, SPTerm -> SPTerm -> SPTerm
mkConj)
    in if [FORMULA f] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FORMULA f]
phis then SPSymbol -> SPTerm
simpTerm SPSymbol
n else
    (SPTerm -> SPTerm -> SPTerm) -> [SPTerm] -> SPTerm
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 SPTerm -> SPTerm -> SPTerm
op ((FORMULA f -> SPTerm) -> [FORMULA f] -> [SPTerm]
forall a b. (a -> b) -> [a] -> [b]
map (Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> FORMULA f
-> SPTerm
forall f e.
FormExtension f =>
Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> FORMULA f
-> SPTerm
transFORMULA Bool
siSo Sign f e
sign IdTypeSPIdMap
idMap FormulaTranslator f e
tr) [FORMULA f]
phis)
  Relation phi1 :: FORMULA f
phi1 c :: Relation
c phi2 :: FORMULA f
phi2 _ -> SPSymbol -> [SPTerm] -> SPTerm
compTerm
    (if Relation
c Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
== Relation
Equivalence then SPSymbol
SPEquiv else SPSymbol
SPImplies)
    [Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> FORMULA f
-> SPTerm
forall f e.
FormExtension f =>
Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> FORMULA f
-> SPTerm
transFORMULA Bool
siSo Sign f e
sign IdTypeSPIdMap
idMap FormulaTranslator f e
tr FORMULA f
phi1, Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> FORMULA f
-> SPTerm
forall f e.
FormExtension f =>
Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> FORMULA f
-> SPTerm
transFORMULA Bool
siSo Sign f e
sign IdTypeSPIdMap
idMap FormulaTranslator f e
tr FORMULA f
phi2]
  Negation phi :: FORMULA f
phi _ -> SPSymbol -> [SPTerm] -> SPTerm
compTerm SPSymbol
SPNot [Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> FORMULA f
-> SPTerm
forall f e.
FormExtension f =>
Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> FORMULA f
-> SPTerm
transFORMULA Bool
siSo Sign f e
sign IdTypeSPIdMap
idMap FormulaTranslator f e
tr FORMULA f
phi]
  Atom b :: Bool
b _ -> SPSymbol -> SPTerm
simpTerm (SPSymbol -> SPTerm) -> SPSymbol -> SPTerm
forall a b. (a -> b) -> a -> b
$ if Bool
b then SPSymbol
SPTrue else SPSymbol
SPFalse
  Predication psymb :: PRED_SYMB
psymb args :: [TERM f]
args _ -> SPSymbol -> [SPTerm] -> SPTerm
compTerm (SPIdentifier -> SPSymbol
spSym (IdTypeSPIdMap -> PRED_SYMB -> SPIdentifier
transPREDSYMB IdTypeSPIdMap
idMap PRED_SYMB
psymb))
           ((TERM f -> SPTerm) -> [TERM f] -> [SPTerm]
forall a b. (a -> b) -> [a] -> [b]
map (Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> TERM f
-> SPTerm
forall f e.
FormExtension f =>
Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> TERM f
-> SPTerm
transTERM Bool
siSo Sign f e
sign IdTypeSPIdMap
idMap FormulaTranslator f e
tr) [TERM f]
args)
  Equation t1 :: TERM f
t1 _ t2 :: TERM f
t2 _ -> -- sortOfTerm t1 == sortOfTerm t2
       SPTerm -> SPTerm -> SPTerm
mkEq (Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> TERM f
-> SPTerm
forall f e.
FormExtension f =>
Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> TERM f
-> SPTerm
transTERM Bool
siSo Sign f e
sign IdTypeSPIdMap
idMap FormulaTranslator f e
tr TERM f
t1) (Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> TERM f
-> SPTerm
forall f e.
FormExtension f =>
Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> TERM f
-> SPTerm
transTERM Bool
siSo Sign f e
sign IdTypeSPIdMap
idMap FormulaTranslator f e
tr TERM f
t2)
  ExtFORMULA phi :: f
phi -> FormulaTranslator f e
tr Sign f e
sign IdTypeSPIdMap
idMap f
phi
  Definedness _ _ -> SPSymbol -> SPTerm
simpTerm SPSymbol
SPTrue -- assume totality
  Membership t :: TERM f
t s :: Id
s _ -> if Bool
siSo then SPSymbol -> SPTerm
simpTerm SPSymbol
SPTrue else
    SPTerm -> (SPIdentifier -> SPTerm) -> Maybe SPIdentifier -> SPTerm
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> SPTerm
forall a. (?callStack::CallStack) => String -> a
error ("SuleCFOL2SoftFOL.tF: no SoftFOL Id found for \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++
                  Id -> ShowS
forall a. Pretty a => a -> ShowS
showDoc Id
s "\""))
          (\ si :: SPIdentifier
si -> SPSymbol -> [SPTerm] -> SPTerm
compTerm (SPIdentifier -> SPSymbol
spSym SPIdentifier
si) [Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> TERM f
-> SPTerm
forall f e.
FormExtension f =>
Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> TERM f
-> SPTerm
transTERM Bool
siSo Sign f e
sign IdTypeSPIdMap
idMap FormulaTranslator f e
tr TERM f
t])
          (Id -> CType -> IdTypeSPIdMap -> Maybe SPIdentifier
lookupSPId Id
s CType
CSort IdTypeSPIdMap
idMap)
  _ -> String -> SPTerm
forall a. (?callStack::CallStack) => String -> a
error
    (String -> SPTerm) -> String -> SPTerm
forall a b. (a -> b) -> a -> b
$ "SuleCFOL2SoftFOL.transFORMULA: unknown FORMULA '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ FORMULA f -> ShowS
forall a. Pretty a => a -> ShowS
showDoc FORMULA f
frm "'"

transTERM :: FormExtension f => Bool -> CSign.Sign f e -> IdTypeSPIdMap
          -> FormulaTranslator f e -> TERM f -> SPTerm
transTERM :: Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> TERM f
-> SPTerm
transTERM siSo :: Bool
siSo sign :: Sign f e
sign idMap :: IdTypeSPIdMap
idMap tr :: FormulaTranslator f e
tr term :: TERM f
term = case TERM f
term of
  Qual_var v :: SPIdentifier
v s :: Id
s _ -> SPTerm -> (SPIdentifier -> SPTerm) -> Maybe SPIdentifier -> SPTerm
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
    (String -> SPTerm
forall a. (?callStack::CallStack) => String -> a
error
         ("SuleCFOL2SoftFOL.tT: no SoftFOL Id found for \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPIdentifier -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SPIdentifier
v "\""))
        (SPSymbol -> SPTerm
simpTerm (SPSymbol -> SPTerm)
-> (SPIdentifier -> SPSymbol) -> SPIdentifier -> SPTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPIdentifier -> SPSymbol
spSym) (Id -> CType -> IdTypeSPIdMap -> Maybe SPIdentifier
lookupSPId (SPIdentifier -> Id
simpleIdToId SPIdentifier
v) (Id -> CType
CVar Id
s) IdTypeSPIdMap
idMap)
  Application opsymb :: OP_SYMB
opsymb args :: [TERM f]
args _ ->
    SPSymbol -> [SPTerm] -> SPTerm
compTerm (SPIdentifier -> SPSymbol
spSym (IdTypeSPIdMap -> OP_SYMB -> SPIdentifier
transOPSYMB IdTypeSPIdMap
idMap OP_SYMB
opsymb))
             ((TERM f -> SPTerm) -> [TERM f] -> [SPTerm]
forall a b. (a -> b) -> [a] -> [b]
map (Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> TERM f
-> SPTerm
forall f e.
FormExtension f =>
Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> TERM f
-> SPTerm
transTERM Bool
siSo Sign f e
sign IdTypeSPIdMap
idMap FormulaTranslator f e
tr) [TERM f]
args)
  Conditional _t1 :: TERM f
_t1 _phi :: FORMULA f
_phi _t2 :: TERM f
_t2 _ ->
    String -> SPTerm
forall a. (?callStack::CallStack) => String -> a
error "SuleCFOL2SoftFOL.transTERM: Conditional terms must be coded out."
  Sorted_term t :: TERM f
t _s :: Id
_s _ -> -- sortOfTerm t isSubsortOf s
    Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> TERM f
-> SPTerm
forall f e.
FormExtension f =>
Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> TERM f
-> SPTerm
transTERM Bool
siSo Sign f e
sign IdTypeSPIdMap
idMap FormulaTranslator f e
tr TERM f
t
  Cast t :: TERM f
t _s :: Id
_s _ -> -- s isSubsortOf sortOfTerm t
    Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> TERM f
-> SPTerm
forall f e.
FormExtension f =>
Bool
-> Sign f e
-> IdTypeSPIdMap
-> FormulaTranslator f e
-> TERM f
-> SPTerm
transTERM Bool
siSo Sign f e
sign IdTypeSPIdMap
idMap FormulaTranslator f e
tr TERM f
t
  _ -> String -> SPTerm
forall a. (?callStack::CallStack) => String -> a
error ("SuleCFOL2SoftFOL.transTERM: unknown TERM '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TERM f -> ShowS
forall a. Pretty a => a -> ShowS
showDoc TERM f
term "'")

isSingleSorted :: CSign.Sign f e -> Bool
isSingleSorted :: Sign f e -> Bool
isSingleSorted sign :: Sign f e
sign =
  Set Id -> Int
forall a. Set a -> Int
Set.size (Sign f e -> Set Id
forall f e. Sign f e -> Set Id
CSign.sortSet Sign f e
sign) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1
  Bool -> Bool -> Bool
&& Set Id -> Bool
forall a. Set a -> Bool
Set.null (Sign f e -> Set Id
forall f e. Sign f e -> Set Id
emptySortSet Sign f e
sign) -- empty sorts need relativization

-- * extract model out of darwin output stored in a proof tree

extractCASLModel :: CASLSign -> ProofTree
  -> Result (CASLSign, [Named (FORMULA ())])
extractCASLModel :: CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA])
extractCASLModel sign :: CASLSign
sign (ProofTree output :: String
output) =
  case Parsec String () [(String, SPTerm)]
-> String -> String -> Either ParseError [(String, SPTerm)]
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse Parsec String () [(String, SPTerm)]
tptpModel "" String
output of
    Right rfs :: [(String, SPTerm)]
rfs -> do
      let idMap :: IdTypeSPIdMap
idMap = (Sign, IdTypeSPIdMap) -> IdTypeSPIdMap
forall a b. (a, b) -> b
snd ((Sign, IdTypeSPIdMap) -> IdTypeSPIdMap)
-> (Sign, IdTypeSPIdMap) -> IdTypeSPIdMap
forall a b. (a -> b) -> a -> b
$ CASLSign -> (Sign, IdTypeSPIdMap)
forall f e. Sign f e -> (Sign, IdTypeSPIdMap)
transSign CASLSign
sign
          rMap :: RMap
rMap = IdTypeSPIdMap -> RMap
getSignMap IdTypeSPIdMap
idMap
          (rs :: [(String, SPTerm)]
rs, fs1 :: [(String, SPTerm)]
fs1) = ((String, SPTerm) -> Bool)
-> [(String, SPTerm)] -> ([(String, SPTerm)], [(String, SPTerm)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "interpretation_atoms") (String -> Bool)
-> ((String, SPTerm) -> String) -> (String, SPTerm) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, SPTerm) -> String
forall a b. (a, b) -> a
fst) [(String, SPTerm)]
rfs
          (ds :: [(String, SPTerm)]
ds, fs2 :: [(String, SPTerm)]
fs2) = ((String, SPTerm) -> Bool)
-> [(String, SPTerm)] -> ([(String, SPTerm)], [(String, SPTerm)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "interpretation_domain") (String -> Bool)
-> ((String, SPTerm) -> String) -> (String, SPTerm) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, SPTerm) -> String
forall a b. (a, b) -> a
fst) [(String, SPTerm)]
fs1
          (dds :: [(String, SPTerm)]
dds, fs3 :: [(String, SPTerm)]
fs3) = ((String, SPTerm) -> Bool)
-> [(String, SPTerm)] -> ([(String, SPTerm)], [(String, SPTerm)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition
            ((String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "interpretation_domain_distinct") (String -> Bool)
-> ((String, SPTerm) -> String) -> (String, SPTerm) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, SPTerm) -> String
forall a b. (a, b) -> a
fst) [(String, SPTerm)]
fs2
          (es :: [String]
es, nm0 :: RMap
nm0) = (([String], RMap) -> (String, SPTerm) -> ([String], RMap))
-> ([String], RMap) -> [(String, SPTerm)] -> ([String], RMap)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ (l :: [String]
l, m :: RMap
m) (_, s :: SPTerm
s) -> let
                           (e :: [String]
e, m2 :: RMap
m2) = Bool -> CASLSign -> RMap -> SPTerm -> ([String], RMap)
typeCheckForm Bool
False CASLSign
sign RMap
m SPTerm
s
                           in ([String]
l [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
e, RMap
m2)) ([], RMap
rMap) [(String, SPTerm)]
rs
          nm :: RMap
nm = (RMap -> (String, SPTerm) -> RMap)
-> RMap -> [(String, SPTerm)] -> RMap
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ m :: RMap
m (_, s :: SPTerm
s) -> ([String], RMap) -> RMap
forall a b. (a, b) -> b
snd (([String], RMap) -> RMap) -> ([String], RMap) -> RMap
forall a b. (a -> b) -> a -> b
$ Bool -> CASLSign -> RMap -> SPTerm -> ([String], RMap)
typeCheckForm Bool
True CASLSign
sign RMap
m SPTerm
s) RMap
nm0
               ([(String, SPTerm)] -> RMap) -> [(String, SPTerm)] -> RMap
forall a b. (a -> b) -> a -> b
$ [(String, SPTerm)]
fs3 [(String, SPTerm)] -> [(String, SPTerm)] -> [(String, SPTerm)]
forall a. [a] -> [a] -> [a]
++ [(String, SPTerm)]
ds [(String, SPTerm)] -> [(String, SPTerm)] -> [(String, SPTerm)]
forall a. [a] -> [a] -> [a]
++ [(String, SPTerm)]
dds
          nops :: RMap
nops = ((CType, Maybe Id) -> Bool) -> RMap -> RMap
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (\ v :: (CType, Maybe Id)
v -> case (CType, Maybe Id)
v of
            (COp _, Nothing) -> Bool
True
            _ -> Bool
False) RMap
nm
          os :: MapSet Id OpType
os = CASLSign -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap CASLSign
sign
          nos :: MapSet Id OpType
nos = ((SPIdentifier, (CType, Maybe Id))
 -> MapSet Id OpType -> MapSet Id OpType)
-> MapSet Id OpType
-> [(SPIdentifier, (CType, Maybe Id))]
-> MapSet Id OpType
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (i :: SPIdentifier
i, ~(COp ot :: OpType
ot, _)) -> Id -> OpType -> MapSet Id OpType -> MapSet Id OpType
addOpTo (SPIdentifier -> Id
simpleIdToId SPIdentifier
i) OpType
ot) MapSet Id OpType
os
            ([(SPIdentifier, (CType, Maybe Id))] -> MapSet Id OpType)
-> [(SPIdentifier, (CType, Maybe Id))] -> MapSet Id OpType
forall a b. (a -> b) -> a -> b
$ RMap -> [(SPIdentifier, (CType, Maybe Id))]
forall k a. Map k a -> [(k, a)]
Map.toList RMap
nops
          nsign :: CASLSign
nsign = CASLSign
sign { opMap :: MapSet Id OpType
opMap = MapSet Id OpType
nos }
          mkWarn :: String -> Diagnosis
mkWarn s :: String
s = DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Warning String
s Range
nullRange
      [Named CASLFORMULA]
doms <- if Set Id -> Bool
forall a. Set a -> Bool
Set.null (CASLSign -> Set Id
forall f e. Sign f e -> Set Id
sortSet CASLSign
sign) then [Named CASLFORMULA] -> Result [Named CASLFORMULA]
forall (m :: * -> *) a. Monad m => a -> m a
return [] else
        ((String, SPTerm) -> Result (Named CASLFORMULA))
-> [(String, SPTerm)] -> Result [Named CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (n :: String
n, f :: SPTerm
f) -> do
          [SPTerm]
diss <- SPTerm -> Result [SPTerm]
getDomElems SPTerm
f
          CASLFORMULA
nf <- CASLSign -> RMap -> [SPTerm] -> Result CASLFORMULA
createDomain CASLSign
sign RMap
nm [SPTerm]
diss
          Named CASLFORMULA -> Result (Named CASLFORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (Named CASLFORMULA -> Result (Named CASLFORMULA))
-> Named CASLFORMULA -> Result (Named CASLFORMULA)
forall a b. (a -> b) -> a -> b
$ String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed String
n CASLFORMULA
nf) [(String, SPTerm)]
ds
      [Named CASLFORMULA]
distfs <- ((String, SPTerm) -> Result (Named CASLFORMULA))
-> [(String, SPTerm)] -> Result [Named CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (n :: String
n, f :: SPTerm
f) -> do
          let fs :: [SPTerm]
fs = SPTerm -> [SPTerm]
splitConjs SPTerm
f
              ets :: [[String]]
ets = (SPTerm -> [String]) -> [SPTerm] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map (([String], RMap) -> [String]
forall a b. (a, b) -> a
fst (([String], RMap) -> [String])
-> (SPTerm -> ([String], RMap)) -> SPTerm -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> CASLSign -> RMap -> SPTerm -> ([String], RMap)
typeCheckForm Bool
False CASLSign
sign RMap
nm) [SPTerm]
fs
              cs :: [([String], SPTerm)]
cs = (([String], SPTerm) -> Bool)
-> [([String], SPTerm)] -> [([String], SPTerm)]
forall a. (a -> Bool) -> [a] -> [a]
filter ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String] -> Bool)
-> (([String], SPTerm) -> [String]) -> ([String], SPTerm) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([String], SPTerm) -> [String]
forall a b. (a, b) -> a
fst) ([([String], SPTerm)] -> [([String], SPTerm)])
-> [([String], SPTerm)] -> [([String], SPTerm)]
forall a b. (a -> b) -> a -> b
$ [[String]] -> [SPTerm] -> [([String], SPTerm)]
forall a b. [a] -> [b] -> [(a, b)]
zip [[String]]
ets [SPTerm]
fs
          Set SPTerm
dts <- (Set SPTerm -> SPTerm -> Result (Set SPTerm))
-> Set SPTerm -> [SPTerm] -> Result (Set SPTerm)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Set SPTerm -> SPTerm -> Result (Set SPTerm)
getUneqElems Set SPTerm
forall a. Set a
Set.empty [SPTerm]
fs
          let ws :: [String]
ws = (SPTerm -> [String]) -> [SPTerm] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((\ (s :: [String]
s, _, _) -> [String]
s)
                              (([String], RMap, Maybe Id) -> [String])
-> (SPTerm -> ([String], RMap, Maybe Id)) -> SPTerm -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLSign
-> Maybe Id -> RMap -> SPTerm -> ([String], RMap, Maybe Id)
typeCheckTerm CASLSign
sign Maybe Id
forall a. Maybe a
Nothing RMap
nm)
                   ([SPTerm] -> [String]) -> [SPTerm] -> [String]
forall a b. (a -> b) -> a -> b
$ Set SPTerm -> [SPTerm]
forall a. Set a -> [a]
Set.toList Set SPTerm
dts
          [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result ((String -> Diagnosis) -> [String] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map String -> Diagnosis
mkWarn [String]
ws) (Maybe () -> Result ()) -> Maybe () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> Maybe ()
forall a. a -> Maybe a
Just ()
          [CASLFORMULA]
tfs <- (([String], SPTerm) -> Result CASLFORMULA)
-> [([String], SPTerm)] -> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CASLSign -> RMap -> SPTerm -> Result CASLFORMULA
forall (m :: * -> *).
MonadFail m =>
CASLSign -> RMap -> SPTerm -> m CASLFORMULA
toForm CASLSign
nsign RMap
nm (SPTerm -> Result CASLFORMULA)
-> (([String], SPTerm) -> SPTerm)
-> ([String], SPTerm)
-> Result CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([String], SPTerm) -> SPTerm
forall a b. (a, b) -> b
snd) [([String], SPTerm)]
cs
          Named CASLFORMULA -> Result (Named CASLFORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (Named CASLFORMULA -> Result (Named CASLFORMULA))
-> Named CASLFORMULA -> Result (Named CASLFORMULA)
forall a b. (a -> b) -> a -> b
$ String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed String
n (CASLFORMULA -> Named CASLFORMULA)
-> CASLFORMULA -> Named CASLFORMULA
forall a b. (a -> b) -> a -> b
$ (() -> ()) -> CASLFORMULA -> CASLFORMULA
forall f. Ord f => (f -> f) -> FORMULA f -> FORMULA f
simplifyFormula () -> ()
forall a. a -> a
id (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [CASLFORMULA]
tfs) [(String, SPTerm)]
dds
      [Named CASLFORMULA]
terms <- ((String, SPTerm) -> Result (Named CASLFORMULA))
-> [(String, SPTerm)] -> Result [Named CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (n :: String
n, f :: SPTerm
f) -> do
          let fs :: [SPTerm]
fs = SPTerm -> [SPTerm]
splitConjs SPTerm
f
              ets :: [[String]]
ets = (SPTerm -> [String]) -> [SPTerm] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map (([String], RMap) -> [String]
forall a b. (a, b) -> a
fst (([String], RMap) -> [String])
-> (SPTerm -> ([String], RMap)) -> SPTerm -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> CASLSign -> RMap -> SPTerm -> ([String], RMap)
typeCheckForm Bool
False CASLSign
sign RMap
nm) [SPTerm]
fs
              (cs :: [([String], SPTerm)]
cs, ws :: [([String], SPTerm)]
ws) = (([String], SPTerm) -> Bool)
-> [([String], SPTerm)]
-> ([([String], SPTerm)], [([String], SPTerm)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String] -> Bool)
-> (([String], SPTerm) -> [String]) -> ([String], SPTerm) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([String], SPTerm) -> [String]
forall a b. (a, b) -> a
fst) ([([String], SPTerm)]
 -> ([([String], SPTerm)], [([String], SPTerm)]))
-> [([String], SPTerm)]
-> ([([String], SPTerm)], [([String], SPTerm)])
forall a b. (a -> b) -> a -> b
$ [[String]] -> [SPTerm] -> [([String], SPTerm)]
forall a b. [a] -> [b] -> [(a, b)]
zip [[String]]
ets [SPTerm]
fs
          [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result ((String -> Diagnosis) -> [String] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map String -> Diagnosis
mkWarn ([String] -> [Diagnosis]) -> [String] -> [Diagnosis]
forall a b. (a -> b) -> a -> b
$ (([String], SPTerm) -> [String])
-> [([String], SPTerm)] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([String], SPTerm) -> [String]
forall a b. (a, b) -> a
fst [([String], SPTerm)]
ws) (Maybe () -> Result ()) -> Maybe () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> Maybe ()
forall a. a -> Maybe a
Just ()
          [CASLFORMULA]
tfs <- (([String], SPTerm) -> Result CASLFORMULA)
-> [([String], SPTerm)] -> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CASLSign -> RMap -> SPTerm -> Result CASLFORMULA
forall (m :: * -> *).
MonadFail m =>
CASLSign -> RMap -> SPTerm -> m CASLFORMULA
toForm CASLSign
nsign RMap
nm (SPTerm -> Result CASLFORMULA)
-> (([String], SPTerm) -> SPTerm)
-> ([String], SPTerm)
-> Result CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([String], SPTerm) -> SPTerm
forall a b. (a, b) -> b
snd) [([String], SPTerm)]
cs
          Named CASLFORMULA -> Result (Named CASLFORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (Named CASLFORMULA -> Result (Named CASLFORMULA))
-> Named CASLFORMULA -> Result (Named CASLFORMULA)
forall a b. (a -> b) -> a -> b
$ String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed String
n (CASLFORMULA -> Named CASLFORMULA)
-> CASLFORMULA -> Named CASLFORMULA
forall a b. (a -> b) -> a -> b
$ (() -> ()) -> CASLFORMULA -> CASLFORMULA
forall f. Ord f => (f -> f) -> FORMULA f -> FORMULA f
simplifyFormula () -> ()
forall a. a -> a
id (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [CASLFORMULA]
tfs) [(String, SPTerm)]
fs3
      [Named CASLFORMULA]
sens <- ((String, SPTerm) -> Result (Named CASLFORMULA))
-> [(String, SPTerm)] -> Result [Named CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (n :: String
n, f :: SPTerm
f) -> do
         CASLFORMULA
cf <- CASLSign -> RMap -> SPTerm -> Result CASLFORMULA
forall (m :: * -> *).
MonadFail m =>
CASLSign -> RMap -> SPTerm -> m CASLFORMULA
toForm CASLSign
nsign RMap
nm SPTerm
f
         Named CASLFORMULA -> Result (Named CASLFORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (Named CASLFORMULA -> Result (Named CASLFORMULA))
-> Named CASLFORMULA -> Result (Named CASLFORMULA)
forall a b. (a -> b) -> a -> b
$ String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed String
n (CASLFORMULA -> Named CASLFORMULA)
-> CASLFORMULA -> Named CASLFORMULA
forall a b. (a -> b) -> a -> b
$ (() -> ()) -> CASLFORMULA -> CASLFORMULA
forall f. Ord f => (f -> f) -> FORMULA f -> FORMULA f
simplifyFormula () -> ()
forall a. a -> a
id CASLFORMULA
cf) [(String, SPTerm)]
rs
      [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result ((String -> Diagnosis) -> [String] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map String -> Diagnosis
mkWarn [String]
es) (Maybe () -> Result ()) -> Maybe () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> Maybe ()
forall a. a -> Maybe a
Just ()
      (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLSign
nsign, [Named CASLFORMULA]
doms [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
distfs [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
terms [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
sens)
    Left err :: ParseError
err -> String -> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result (CASLSign, [Named CASLFORMULA]))
-> String -> Result (CASLSign, [Named CASLFORMULA])
forall a b. (a -> b) -> a -> b
$ ParseError -> String
showErr ParseError
err

type RMap = Map.Map SPIdentifier (CType, Maybe Id)

getSignMap :: IdTypeSPIdMap -> RMap
getSignMap :: IdTypeSPIdMap -> RMap
getSignMap =
  ((Id, Map CType SPIdentifier) -> RMap -> RMap)
-> RMap -> [(Id, Map CType SPIdentifier)] -> RMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (i :: Id
i, m :: Map CType SPIdentifier
m) g :: RMap
g -> ((CType, SPIdentifier) -> RMap -> RMap)
-> RMap -> [(CType, SPIdentifier)] -> RMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (t :: CType
t, s :: SPIdentifier
s) -> case CType
t of
       CSort -> SPIdentifier -> (CType, Maybe Id) -> RMap -> RMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SPIdentifier
s (PredType -> CType
CPred (PredType -> CType) -> PredType -> CType
forall a b. (a -> b) -> a -> b
$ [Id] -> PredType
PredType [Id
i], Maybe Id
forall a. Maybe a
Nothing)
       _ -> SPIdentifier -> (CType, Maybe Id) -> RMap -> RMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SPIdentifier
s (CType
t, Id -> Maybe Id
forall a. a -> Maybe a
Just Id
i)) RMap
g ([(CType, SPIdentifier)] -> RMap)
-> [(CType, SPIdentifier)] -> RMap
forall a b. (a -> b) -> a -> b
$ Map CType SPIdentifier -> [(CType, SPIdentifier)]
forall k a. Map k a -> [(k, a)]
Map.toList Map CType SPIdentifier
m)
         RMap
forall k a. Map k a
Map.empty ([(Id, Map CType SPIdentifier)] -> RMap)
-> (IdTypeSPIdMap -> [(Id, Map CType SPIdentifier)])
-> IdTypeSPIdMap
-> RMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IdTypeSPIdMap -> [(Id, Map CType SPIdentifier)]
forall k a. Map k a -> [(k, a)]
Map.toList

splitConjs :: SPTerm -> [SPTerm]
splitConjs :: SPTerm -> [SPTerm]
splitConjs trm :: SPTerm
trm = case SPTerm
trm of
  SPComplexTerm SPAnd args :: [SPTerm]
args ->
     (SPTerm -> [SPTerm]) -> [SPTerm] -> [SPTerm]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SPTerm -> [SPTerm]
splitConjs [SPTerm]
args
  _ -> [SPTerm
trm]

getUneqElems :: Set.Set SPTerm -> SPTerm -> Result (Set.Set SPTerm)
getUneqElems :: Set SPTerm -> SPTerm -> Result (Set SPTerm)
getUneqElems s :: Set SPTerm
s trm :: SPTerm
trm = case SPTerm
trm of
  SPComplexTerm SPNot [SPComplexTerm SPEqual [a1 :: SPTerm
a1, a2 :: SPTerm
a2]] ->
      Set SPTerm -> Result (Set SPTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set SPTerm -> Result (Set SPTerm))
-> Set SPTerm -> Result (Set SPTerm)
forall a b. (a -> b) -> a -> b
$ SPTerm -> Set SPTerm -> Set SPTerm
forall a. Ord a => a -> Set a -> Set a
Set.insert SPTerm
a2 (Set SPTerm -> Set SPTerm) -> Set SPTerm -> Set SPTerm
forall a b. (a -> b) -> a -> b
$ SPTerm -> Set SPTerm -> Set SPTerm
forall a. Ord a => a -> Set a -> Set a
Set.insert SPTerm
a1 Set SPTerm
s
  _ -> String -> Result (Set SPTerm)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result (Set SPTerm)) -> String -> Result (Set SPTerm)
forall a b. (a -> b) -> a -> b
$ "unexpected disjointness formula: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPTerm -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SPTerm
trm ""

splitDisjs :: SPTerm -> [SPTerm]
splitDisjs :: SPTerm -> [SPTerm]
splitDisjs trm :: SPTerm
trm = case SPTerm
trm of
  SPComplexTerm SPOr args :: [SPTerm]
args ->
     (SPTerm -> [SPTerm]) -> [SPTerm] -> [SPTerm]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SPTerm -> [SPTerm]
splitDisjs [SPTerm]
args
  _ -> [SPTerm
trm]

getDomElems :: SPTerm -> Result [SPTerm]
getDomElems :: SPTerm -> Result [SPTerm]
getDomElems trm :: SPTerm
trm = case SPTerm
trm of
  SPQuantTerm SPForall [var :: SPTerm
var] frm :: SPTerm
frm ->
      (SPTerm -> Result SPTerm) -> [SPTerm] -> Result [SPTerm]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ t :: SPTerm
t -> case SPTerm
t of
        SPComplexTerm SPEqual [a1 :: SPTerm
a1, a2 :: SPTerm
a2]
          | SPTerm
var SPTerm -> SPTerm -> Bool
forall a. Eq a => a -> a -> Bool
== SPTerm
a1 -> SPTerm -> Result SPTerm
forall (m :: * -> *) a. Monad m => a -> m a
return SPTerm
a2
          | SPTerm
var SPTerm -> SPTerm -> Bool
forall a. Eq a => a -> a -> Bool
== SPTerm
a2 -> SPTerm -> Result SPTerm
forall (m :: * -> *) a. Monad m => a -> m a
return SPTerm
a1
        _ -> String -> Result SPTerm
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result SPTerm) -> String -> Result SPTerm
forall a b. (a -> b) -> a -> b
$ "expecting equation with " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPTerm -> String
forall a. Show a => a -> String
show SPTerm
var
             String -> ShowS
forall a. [a] -> [a] -> [a]
++ ", got: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPTerm -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SPTerm
t "") ([SPTerm] -> Result [SPTerm]) -> [SPTerm] -> Result [SPTerm]
forall a b. (a -> b) -> a -> b
$ SPTerm -> [SPTerm]
splitDisjs SPTerm
frm
  _ -> String -> Result [SPTerm]
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result [SPTerm]) -> String -> Result [SPTerm]
forall a b. (a -> b) -> a -> b
$ "expecting simple quantified disjunction, got: "
       String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPTerm -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SPTerm
trm ""

createDomain :: CASLSign -> RMap -> [SPTerm] -> Result (FORMULA ())
createDomain :: CASLSign -> RMap -> [SPTerm] -> Result CASLFORMULA
createDomain sign :: CASLSign
sign m :: RMap
m l :: [SPTerm]
l = do
  let es :: [([String], Maybe Id)]
es = (SPTerm -> ([String], Maybe Id))
-> [SPTerm] -> [([String], Maybe Id)]
forall a b. (a -> b) -> [a] -> [b]
map ((\ (e :: [String]
e, _, s :: Maybe Id
s) -> ([String]
e, Maybe Id
s)) (([String], RMap, Maybe Id) -> ([String], Maybe Id))
-> (SPTerm -> ([String], RMap, Maybe Id))
-> SPTerm
-> ([String], Maybe Id)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLSign
-> Maybe Id -> RMap -> SPTerm -> ([String], RMap, Maybe Id)
typeCheckTerm CASLSign
sign Maybe Id
forall a. Maybe a
Nothing RMap
m) [SPTerm]
l
  [Id]
tys <- (([String], Maybe Id) -> Result Id)
-> [([String], Maybe Id)] -> Result [Id]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (e :: [String]
e, ms :: Maybe Id
ms) -> case Maybe Id
ms of
          Just s :: Id
s -> Id -> Result Id
forall (m :: * -> *) a. Monad m => a -> m a
return Id
s
          _ -> String -> Result Id
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result Id) -> String -> Result Id
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String]
e) [([String], Maybe Id)]
es
  [CASLFORMULA]
cs <- ([(Id, SPTerm)] -> Result CASLFORMULA)
-> [[(Id, SPTerm)]] -> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ ds :: [(Id, SPTerm)]
ds -> do
        ts :: [TERM ()]
ts@(trm :: TERM ()
trm : r :: [TERM ()]
r) <- ((Id, SPTerm) -> Result (TERM ()))
-> [(Id, SPTerm)] -> Result [TERM ()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (RMap -> SPTerm -> Result (TERM ())
forall (m :: * -> *). MonadFail m => RMap -> SPTerm -> m (TERM ())
toTERM RMap
m (SPTerm -> Result (TERM ()))
-> ((Id, SPTerm) -> SPTerm) -> (Id, SPTerm) -> Result (TERM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id, SPTerm) -> SPTerm
forall a b. (a, b) -> b
snd) [(Id, SPTerm)]
ds
        let mtys :: [Id]
mtys = CASLSign -> (Id -> Id) -> [Id] -> [Id]
forall f e a. Sign f e -> (a -> Id) -> [a] -> [a]
keepMinimals CASLSign
sign Id -> Id
forall a. a -> a
id ([Id] -> [Id]) -> ([Set Id] -> [Id]) -> [Set Id] -> [Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Id -> [Id]
forall a. Set a -> [a]
Set.toList (Set Id -> [Id]) -> ([Set Id] -> Set Id) -> [Set Id] -> [Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set Id -> Set Id -> Set Id) -> [Set Id] -> Set Id
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection
                  ([Set Id] -> [Id]) -> [Set Id] -> [Id]
forall a b. (a -> b) -> a -> b
$ ((Id, SPTerm) -> Set Id) -> [(Id, SPTerm)] -> [Set Id]
forall a b. (a -> b) -> [a] -> [b]
map (\ (ty :: Id
ty, _) -> Id -> Set Id -> Set Id
forall a. Ord a => a -> Set a -> Set a
Set.insert Id
ty (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Id -> CASLSign -> Set Id
forall f e. Id -> Sign f e -> Set Id
supersortsOf Id
ty CASLSign
sign) [(Id, SPTerm)]
ds
        case [Id]
mtys of
          [] -> String -> Result CASLFORMULA
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result CASLFORMULA) -> String -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ "no common supersort found for: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Id, SPTerm)] -> ShowS
forall a. Pretty a => a -> ShowS
showDoc [(Id, SPTerm)]
ds ""
          ty :: Id
ty : _ -> do
            let v :: VAR_DECL
v = String -> Id -> VAR_DECL
mkVarDeclStr "X" Id
ty
            CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Result CASLFORMULA)
-> CASLFORMULA -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL
v]
              (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ if [TERM ()] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TERM ()]
r then TERM () -> TERM () -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkStEq (VAR_DECL -> TERM ()
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
v) TERM ()
trm else
                   [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
disjunct ([CASLFORMULA] -> CASLFORMULA) -> [CASLFORMULA] -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ (TERM () -> CASLFORMULA) -> [TERM ()] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (TERM () -> TERM () -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkStEq (TERM () -> TERM () -> CASLFORMULA)
-> TERM () -> TERM () -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ VAR_DECL -> TERM ()
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
v) [TERM ()]
ts)
    ([[(Id, SPTerm)]] -> Result [CASLFORMULA])
-> ([(Id, SPTerm)] -> [[(Id, SPTerm)]])
-> [(Id, SPTerm)]
-> Result [CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Id, SPTerm) -> (Id, SPTerm) -> Bool)
-> [(Id, SPTerm)] -> [[(Id, SPTerm)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
Rel.partList
      ((Id -> Id -> Bool)
-> ((Id, SPTerm) -> Id) -> (Id, SPTerm) -> (Id, SPTerm) -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on (Bool -> CASLSign -> Id -> Id -> Bool
forall f e. Bool -> Sign f e -> Id -> Id -> Bool
haveCommonSupersorts Bool
True CASLSign
sign) (Id, SPTerm) -> Id
forall a b. (a, b) -> a
fst) ([(Id, SPTerm)] -> Result [CASLFORMULA])
-> [(Id, SPTerm)] -> Result [CASLFORMULA]
forall a b. (a -> b) -> a -> b
$ [Id] -> [SPTerm] -> [(Id, SPTerm)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Id]
tys [SPTerm]
l
  CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Result CASLFORMULA)
-> CASLFORMULA -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [CASLFORMULA]
cs

typeCheckForm :: Bool -> CASLSign -> RMap -> SPTerm -> ([String], RMap)
typeCheckForm :: Bool -> CASLSign -> RMap -> SPTerm -> ([String], RMap)
typeCheckForm rev :: Bool
rev sign :: CASLSign
sign m :: RMap
m trm :: SPTerm
trm =
  let srts :: Set Id
srts = CASLSign -> Set Id
forall f e. Sign f e -> Set Id
sortSet CASLSign
sign
      aty :: Maybe Id
aty = if Set Id -> Int
forall a. Set a -> Int
Set.size Set Id
srts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 then Id -> Maybe Id
forall a. a -> Maybe a
Just (Id -> Maybe Id) -> Id -> Maybe Id
forall a b. (a -> b) -> a -> b
$ Set Id -> Id
forall a. Set a -> a
Set.findMin Set Id
srts else Maybe Id
forall a. Maybe a
Nothing
  in case SPTerm
trm of
    SPQuantTerm _ vars :: [SPTerm]
vars frm :: SPTerm
frm -> let
        vs :: [SPIdentifier]
vs = (SPTerm -> [SPIdentifier]) -> [SPTerm] -> [SPIdentifier]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SPTerm -> [SPIdentifier]
getVars [SPTerm]
vars
        rm :: RMap
rm = (SPIdentifier -> RMap -> RMap) -> RMap -> [SPIdentifier] -> RMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SPIdentifier -> RMap -> RMap
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete RMap
m [SPIdentifier]
vs
        (errs :: [String]
errs, nm :: RMap
nm) = Bool -> CASLSign -> RMap -> SPTerm -> ([String], RMap)
typeCheckForm Bool
rev CASLSign
sign RMap
rm SPTerm
frm
        m2 :: RMap
m2 = (SPIdentifier -> RMap -> RMap) -> RMap -> [SPIdentifier] -> RMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SPIdentifier -> RMap -> RMap
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete RMap
nm [SPIdentifier]
vs
        in ([String]
errs, RMap -> RMap -> RMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union RMap
m RMap
m2)
    SPComplexTerm SPEqual [a1 :: SPTerm
a1, a2 :: SPTerm
a2] -> let
        (r1 :: [String]
r1, m1 :: RMap
m1, ety :: Maybe Id
ety) = CASLSign
-> Maybe Id
-> RMap
-> SPTerm
-> SPTerm
-> ([String], RMap, Maybe Id)
typeCheckEq CASLSign
sign Maybe Id
aty RMap
m SPTerm
a1 SPTerm
a2
        in case Maybe Id
ety of
             Nothing -> ([String]
r1, RMap
m1)
             Just _ -> let
               (r2 :: [String]
r2, m2 :: RMap
m2, _) = CASLSign
-> Maybe Id
-> RMap
-> SPTerm
-> SPTerm
-> ([String], RMap, Maybe Id)
typeCheckEq CASLSign
sign Maybe Id
ety RMap
m1 SPTerm
a2 SPTerm
a1
               in ([String]
r2, RMap
m2)
    SPComplexTerm (SPCustomSymbol cst :: SPIdentifier
cst) args :: [SPTerm]
args ->
        case SPIdentifier -> RMap -> Maybe (CType, Maybe Id)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SPIdentifier
cst RMap
m of
          Just (CPred pt :: PredType
pt, _) | [SPTerm] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SPTerm]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (PredType -> [Id]
predArgs PredType
pt) ->
            (([String], RMap) -> (Id, SPTerm) -> ([String], RMap))
-> ([String], RMap) -> [(Id, SPTerm)] -> ([String], RMap)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ (b :: [String]
b, p :: RMap
p) (s :: Id
s, a :: SPTerm
a) -> let
                     (nb :: [String]
nb, nm :: RMap
nm, _) = CASLSign
-> Maybe Id -> RMap -> SPTerm -> ([String], RMap, Maybe Id)
typeCheckTerm CASLSign
sign (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
s) RMap
p SPTerm
a
                     in ([String]
b [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
nb, RMap
nm))
                      ([], RMap
m) ([(Id, SPTerm)] -> ([String], RMap))
-> [(Id, SPTerm)] -> ([String], RMap)
forall a b. (a -> b) -> a -> b
$ [Id] -> [SPTerm] -> [(Id, SPTerm)]
forall a b. [a] -> [b] -> [(a, b)]
zip (PredType -> [Id]
predArgs PredType
pt) [SPTerm]
args
          _ -> (["unknown predicate: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
cst], RMap
m)
    SPComplexTerm _ args :: [SPTerm]
args ->
      (([String], RMap) -> SPTerm -> ([String], RMap))
-> ([String], RMap) -> [SPTerm] -> ([String], RMap)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ (b :: [String]
b, p :: RMap
p) a :: SPTerm
a -> let
           (nb :: [String]
nb, nm :: RMap
nm) = Bool -> CASLSign -> RMap -> SPTerm -> ([String], RMap)
typeCheckForm Bool
rev CASLSign
sign RMap
p SPTerm
a
           in ([String]
b [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
nb, RMap
nm)) ([], RMap
m) ([SPTerm] -> ([String], RMap)) -> [SPTerm] -> ([String], RMap)
forall a b. (a -> b) -> a -> b
$ if Bool
rev then [SPTerm] -> [SPTerm]
forall a. [a] -> [a]
reverse [SPTerm]
args else [SPTerm]
args

typeCheckEq :: CASLSign -> Maybe SORT -> RMap -> SPTerm -> SPTerm
  -> ([String], RMap, Maybe SORT)
typeCheckEq :: CASLSign
-> Maybe Id
-> RMap
-> SPTerm
-> SPTerm
-> ([String], RMap, Maybe Id)
typeCheckEq sign :: CASLSign
sign aty :: Maybe Id
aty m :: RMap
m a1 :: SPTerm
a1 a2 :: SPTerm
a2 = let
    (r1 :: [String]
r1, m1 :: RMap
m1, ty1 :: Maybe Id
ty1) = CASLSign
-> Maybe Id -> RMap -> SPTerm -> ([String], RMap, Maybe Id)
typeCheckTerm CASLSign
sign Maybe Id
aty RMap
m SPTerm
a1
    (r2 :: [String]
r2, m2 :: RMap
m2, ty2 :: Maybe Id
ty2) = CASLSign
-> Maybe Id -> RMap -> SPTerm -> ([String], RMap, Maybe Id)
typeCheckTerm CASLSign
sign Maybe Id
aty RMap
m1 SPTerm
a2
    in case (Maybe Id
ty1, Maybe Id
ty2) of
             (Just s1 :: Id
s1, Just s2 :: Id
s2) ->
                ([String]
r1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
r2
                 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ "different types " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Id, Id) -> String
forall a. Show a => a -> String
show (Id
s1, Id
s2) String -> ShowS
forall a. [a] -> [a] -> [a]
++ " in equation: "
                      String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPTerm -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SPTerm
a1 " = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPTerm -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SPTerm
a2 ""
                    | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> CASLSign -> Id -> Id -> Bool
forall f e. Bool -> Sign f e -> Id -> Id -> Bool
haveCommonSupersorts Bool
True CASLSign
sign Id
s1 Id
s2], RMap
m2, Maybe Id
forall a. Maybe a
Nothing)
             (Nothing, _) -> ([String]
r1, RMap
m2, Maybe Id
ty2)
             (_, Nothing) -> ([String]
r1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
r2, RMap
m2, Maybe Id
ty1)

typeCheckTerm :: CASLSign -> Maybe SORT -> RMap -> SPTerm
  -> ([String], RMap, Maybe SORT)
typeCheckTerm :: CASLSign
-> Maybe Id -> RMap -> SPTerm -> ([String], RMap, Maybe Id)
typeCheckTerm sign :: CASLSign
sign ty :: Maybe Id
ty m :: RMap
m trm :: SPTerm
trm =
  let srts :: Set Id
srts = CASLSign -> Set Id
forall f e. Sign f e -> Set Id
sortSet CASLSign
sign
      aty :: Maybe Id
aty = if Set Id -> Int
forall a. Set a -> Int
Set.size Set Id
srts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 then Id -> Maybe Id
forall a. a -> Maybe a
Just (Id -> Maybe Id) -> Id -> Maybe Id
forall a b. (a -> b) -> a -> b
$ Set Id -> Id
forall a. Set a -> a
Set.findMin Set Id
srts else Maybe Id
forall a. Maybe a
Nothing
  in case SPTerm
trm of
    SPComplexTerm (SPCustomSymbol cst :: SPIdentifier
cst) args :: [SPTerm]
args -> case SPIdentifier -> RMap -> Maybe (CType, Maybe Id)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SPIdentifier
cst RMap
m of
      Nothing -> let
          (fb :: [String]
fb, fm :: RMap
fm, aTys :: [Maybe Id]
aTys) = (SPTerm
 -> ([String], RMap, [Maybe Id]) -> ([String], RMap, [Maybe Id]))
-> ([String], RMap, [Maybe Id])
-> [SPTerm]
-> ([String], RMap, [Maybe Id])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ a :: SPTerm
a (b :: [String]
b, p :: RMap
p, tys :: [Maybe Id]
tys) -> let
                     (nb :: [String]
nb, nm :: RMap
nm, tya :: Maybe Id
tya) = CASLSign
-> Maybe Id -> RMap -> SPTerm -> ([String], RMap, Maybe Id)
typeCheckTerm CASLSign
sign Maybe Id
aty RMap
p SPTerm
a
                     in ([String]
b [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
nb, RMap
nm, Maybe Id
tya Maybe Id -> [Maybe Id] -> [Maybe Id]
forall a. a -> [a] -> [a]
: [Maybe Id]
tys)) ([], RMap
m, []) [SPTerm]
args
          in case Maybe Id
ty of
               Just r :: Id
r | (Maybe Id -> Bool) -> [Maybe Id] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Maybe Id -> Bool
forall a. Maybe a -> Bool
isJust [Maybe Id]
aTys ->
                 if [SPTerm] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SPTerm]
args Bool -> Bool -> Bool
&& SPIdentifier -> Bool
isVar SPIdentifier
cst then
                     ([String]
fb, SPIdentifier -> (CType, Maybe Id) -> RMap -> RMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SPIdentifier
cst (Id -> CType
CVar Id
r, Maybe Id
forall a. Maybe a
Nothing) RMap
fm, Maybe Id
ty)
                 else ([String]
fb, SPIdentifier -> (CType, Maybe Id) -> RMap -> RMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SPIdentifier
cst
                        (OpType -> CType
COp (OpType -> CType) -> OpType -> CType
forall a b. (a -> b) -> a -> b
$ [Id] -> Id -> OpType
mkTotOpType ([Maybe Id] -> [Id]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Id]
aTys) Id
r, Maybe Id
forall a. Maybe a
Nothing) RMap
fm
                      , Maybe Id
ty)
               _ -> (["no type for: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPTerm -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SPTerm
trm ""], RMap
fm, Maybe Id
ty)
      Just (COp ot :: OpType
ot, _) -> let
          aTys :: [Id]
aTys = OpType -> [Id]
opArgs OpType
ot
          rTy :: Id
rTy = OpType -> Id
opRes OpType
ot
          (fb :: [String]
fb, fm :: RMap
fm) = (([String], RMap) -> (Id, SPTerm) -> ([String], RMap))
-> ([String], RMap) -> [(Id, SPTerm)] -> ([String], RMap)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ (b :: [String]
b, p :: RMap
p) (s :: Id
s, a :: SPTerm
a) -> let
                     (nb :: [String]
nb, nm :: RMap
nm, _) = CASLSign
-> Maybe Id -> RMap -> SPTerm -> ([String], RMap, Maybe Id)
typeCheckTerm CASLSign
sign (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
s) RMap
p SPTerm
a
                     in ([String]
b [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
nb, RMap
nm)) ([], RMap
m) ([(Id, SPTerm)] -> ([String], RMap))
-> [(Id, SPTerm)] -> ([String], RMap)
forall a b. (a -> b) -> a -> b
$ [Id] -> [SPTerm] -> [(Id, SPTerm)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Id]
aTys [SPTerm]
args
          aTyL :: Int
aTyL = [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Id]
aTys
          argL :: Int
argL = [SPTerm] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SPTerm]
args
          in ([String]
fb [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
              ["expected " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
aTyL String -> ShowS
forall a. [a] -> [a] -> [a]
++ " arguments, but found "
               String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
argL String -> ShowS
forall a. [a] -> [a] -> [a]
++ " for: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
cst | Int
aTyL Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
argL]
              [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ case Maybe Id
ty of
              Just r :: Id
r -> ["expected result sort " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ ", but found "
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
rTy String -> ShowS
forall a. [a] -> [a] -> [a]
++ " for: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
cst | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ CASLSign -> Id -> Id -> Bool
forall f e. Sign f e -> Id -> Id -> Bool
leqSort CASLSign
sign Id
rTy Id
r ]
              _ -> [], RMap
fm, Id -> Maybe Id
forall a. a -> Maybe a
Just Id
rTy)
      Just (CVar s2 :: Id
s2, _) ->
        (["unexpected arguments for variable: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
cst | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [SPTerm] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SPTerm]
args]
         [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ case Maybe Id
ty of
              Just r :: Id
r -> ["expected variable sort " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ ", but found "
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
s2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " for: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
cst | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ CASLSign -> Id -> Id -> Bool
forall f e. Sign f e -> Id -> Id -> Bool
leqSort CASLSign
sign Id
s2 Id
r ]
              _ -> [], RMap
m, Id -> Maybe Id
forall a. a -> Maybe a
Just Id
s2)
      _ -> (["unexpected predicate in term: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPTerm -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SPTerm
trm ""], RMap
m, Maybe Id
ty)
    _ -> (["unexpected term: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPTerm -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SPTerm
trm ""], RMap
m, Maybe Id
ty)

toForm :: Fail.MonadFail m => CASLSign -> RMap -> SPTerm -> m (FORMULA ())
toForm :: CASLSign -> RMap -> SPTerm -> m CASLFORMULA
toForm sign :: CASLSign
sign m :: RMap
m t :: SPTerm
t = case SPTerm
t of
    SPQuantTerm q :: SPQuantSym
q vars :: [SPTerm]
vars frm :: SPTerm
frm -> do
        let vs :: [SPIdentifier]
vs = (SPTerm -> [SPIdentifier]) -> [SPTerm] -> [SPIdentifier]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SPTerm -> [SPIdentifier]
getVars [SPTerm]
vars
            rm :: RMap
rm = (SPIdentifier -> RMap -> RMap) -> RMap -> [SPIdentifier] -> RMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SPIdentifier -> RMap -> RMap
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete RMap
m [SPIdentifier]
vs
            (b :: [String]
b, nm :: RMap
nm) = Bool -> CASLSign -> RMap -> SPTerm -> ([String], RMap)
typeCheckForm Bool
False CASLSign
sign RMap
rm SPTerm
frm
            nvs :: [VAR_DECL]
nvs = (SPTerm -> Maybe VAR_DECL) -> [SPTerm] -> [VAR_DECL]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (RMap -> SPTerm -> Maybe VAR_DECL
forall (m :: * -> *). MonadFail m => RMap -> SPTerm -> m VAR_DECL
toVar RMap
nm) [SPTerm]
vars
        CASLFORMULA
nf <- CASLSign -> RMap -> SPTerm -> m CASLFORMULA
forall (m :: * -> *).
MonadFail m =>
CASLSign -> RMap -> SPTerm -> m CASLFORMULA
toForm CASLSign
sign RMap
nm SPTerm
frm
        if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
b then CASLFORMULA -> m CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> m CASLFORMULA) -> CASLFORMULA -> m CASLFORMULA
forall a b. (a -> b) -> a -> b
$ QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification (SPQuantSym -> QUANTIFIER
toQuant SPQuantSym
q) [VAR_DECL]
nvs CASLFORMULA
nf Range
nullRange
           else String -> m CASLFORMULA
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m CASLFORMULA) -> String -> m CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String]
b
    SPComplexTerm SPEqual [a1 :: SPTerm
a1, a2 :: SPTerm
a2] -> do
        TERM ()
t1 <- RMap -> SPTerm -> m (TERM ())
forall (m :: * -> *). MonadFail m => RMap -> SPTerm -> m (TERM ())
toTERM RMap
m SPTerm
a1
        TERM ()
t2 <- RMap -> SPTerm -> m (TERM ())
forall (m :: * -> *). MonadFail m => RMap -> SPTerm -> m (TERM ())
toTERM RMap
m SPTerm
a2
        CASLFORMULA -> m CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> m CASLFORMULA) -> CASLFORMULA -> m CASLFORMULA
forall a b. (a -> b) -> a -> b
$ TERM () -> TERM () -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM ()
t1 TERM ()
t2
    SPComplexTerm (SPCustomSymbol cst :: SPIdentifier
cst) args :: [SPTerm]
args ->
        case SPIdentifier -> RMap -> Maybe (CType, Maybe Id)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SPIdentifier
cst RMap
m of
          Just (CPred pt :: PredType
pt, mi :: Maybe Id
mi) | [SPTerm] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SPTerm]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (PredType -> [Id]
predArgs PredType
pt) -> do
              [TERM ()]
ts <- (SPTerm -> m (TERM ())) -> [SPTerm] -> m [TERM ()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (RMap -> SPTerm -> m (TERM ())
forall (m :: * -> *). MonadFail m => RMap -> SPTerm -> m (TERM ())
toTERM RMap
m) [SPTerm]
args
              case Maybe Id
mi of
                Nothing -> case [SPTerm]
args of
                  [_] -> CASLFORMULA -> m CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return CASLFORMULA
forall f. FORMULA f
trueForm
                  _ -> String -> m CASLFORMULA
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m CASLFORMULA) -> String -> m CASLFORMULA
forall a b. (a -> b) -> a -> b
$ "unkown predicate: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
cst
                Just i :: Id
i -> CASLFORMULA -> m CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> m CASLFORMULA) -> CASLFORMULA -> m CASLFORMULA
forall a b. (a -> b) -> a -> b
$ PRED_SYMB -> [TERM ()] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication
                      (Id -> PRED_TYPE -> PRED_SYMB
mkQualPred Id
i (PRED_TYPE -> PRED_SYMB) -> PRED_TYPE -> PRED_SYMB
forall a b. (a -> b) -> a -> b
$ PredType -> PRED_TYPE
toPRED_TYPE PredType
pt) [TERM ()]
ts
          _ -> String -> m CASLFORMULA
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m CASLFORMULA) -> String -> m CASLFORMULA
forall a b. (a -> b) -> a -> b
$ "inconsistent pred symbol: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
cst
    SPComplexTerm symb :: SPSymbol
symb args :: [SPTerm]
args -> do
         [CASLFORMULA]
fs <- (SPTerm -> m CASLFORMULA) -> [SPTerm] -> m [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CASLSign -> RMap -> SPTerm -> m CASLFORMULA
forall (m :: * -> *).
MonadFail m =>
CASLSign -> RMap -> SPTerm -> m CASLFORMULA
toForm CASLSign
sign RMap
m) [SPTerm]
args
         case (SPSymbol
symb, [CASLFORMULA]
fs) of
           (SPNot, [f :: CASLFORMULA
f]) -> CASLFORMULA -> m CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
mkNeg CASLFORMULA
f)
           (SPImplies, [f1 :: CASLFORMULA
f1, f2 :: CASLFORMULA
f2]) -> CASLFORMULA -> m CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl CASLFORMULA
f1 CASLFORMULA
f2)
           -- During parsing, "f2 if f1" is saved as "Relation f1 RevImpl f2 _"
           (SPImplied, [f2 :: CASLFORMULA
f2, f1 :: CASLFORMULA
f1]) -> CASLFORMULA -> m CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation CASLFORMULA
f1 Relation
RevImpl CASLFORMULA
f2 Range
nullRange)
           (SPEquiv, [f1 :: CASLFORMULA
f1, f2 :: CASLFORMULA
f2]) -> CASLFORMULA -> m CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkEqv CASLFORMULA
f1 CASLFORMULA
f2)
           (SPAnd, _) -> CASLFORMULA -> m CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [CASLFORMULA]
fs)
           (SPOr, _) -> CASLFORMULA -> m CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return ([CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
disjunct [CASLFORMULA]
fs)
           (SPTrue, []) -> CASLFORMULA -> m CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return CASLFORMULA
forall f. FORMULA f
trueForm
           (SPFalse, []) -> CASLFORMULA -> m CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return CASLFORMULA
forall f. FORMULA f
falseForm
           _ -> String -> m CASLFORMULA
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m CASLFORMULA) -> String -> m CASLFORMULA
forall a b. (a -> b) -> a -> b
$ "wrong boolean formula: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPTerm -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SPTerm
t ""

toTERM :: Fail.MonadFail m => RMap -> SPTerm -> m (TERM ())
toTERM :: RMap -> SPTerm -> m (TERM ())
toTERM m :: RMap
m spt :: SPTerm
spt = case SPTerm
spt of
  SPComplexTerm (SPCustomSymbol cst :: SPIdentifier
cst) args :: [SPTerm]
args -> case SPIdentifier -> RMap -> Maybe (CType, Maybe Id)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SPIdentifier
cst RMap
m of
    Just (CVar s :: Id
s, _) | [SPTerm] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SPTerm]
args -> TERM () -> m (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM () -> m (TERM ())) -> TERM () -> m (TERM ())
forall a b. (a -> b) -> a -> b
$ SPIdentifier -> Id -> Range -> TERM ()
forall f. SPIdentifier -> Id -> Range -> TERM f
Qual_var SPIdentifier
cst Id
s Range
nullRange
    Just (COp ot :: OpType
ot, mi :: Maybe Id
mi) | [SPTerm] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SPTerm]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (OpType -> [Id]
opArgs OpType
ot) -> do
      [TERM ()]
ts <- (SPTerm -> m (TERM ())) -> [SPTerm] -> m [TERM ()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (RMap -> SPTerm -> m (TERM ())
forall (m :: * -> *). MonadFail m => RMap -> SPTerm -> m (TERM ())
toTERM RMap
m) [SPTerm]
args
      TERM () -> m (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM () -> m (TERM ())) -> TERM () -> m (TERM ())
forall a b. (a -> b) -> a -> b
$ OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name (case Maybe Id
mi of
              Just i :: Id
i -> Id
i
              _ -> SPIdentifier -> Id
simpleIdToId SPIdentifier
cst) (OpType -> OP_TYPE
toOP_TYPE OpType
ot) Range
nullRange)
        [TERM ()]
ts Range
nullRange
    _ -> String -> m (TERM ())
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m (TERM ())) -> String -> m (TERM ())
forall a b. (a -> b) -> a -> b
$ "cannot reconstruct term: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPTerm -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SPTerm
spt ""
  _ -> String -> m (TERM ())
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m (TERM ())) -> String -> m (TERM ())
forall a b. (a -> b) -> a -> b
$ "cannot reconstruct term: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPTerm -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SPTerm
spt ""

toQuant :: SPQuantSym -> QUANTIFIER
toQuant :: SPQuantSym -> QUANTIFIER
toQuant sp :: SPQuantSym
sp = case SPQuantSym
sp of
  SPForall -> QUANTIFIER
Universal
  SPExists -> QUANTIFIER
Existential
  _ -> String -> QUANTIFIER
forall a. (?callStack::CallStack) => String -> a
error "toQuant"

toVar :: Fail.MonadFail m => RMap -> SPTerm -> m VAR_DECL
toVar :: RMap -> SPTerm -> m VAR_DECL
toVar m :: RMap
m sp :: SPTerm
sp = case SPTerm
sp of
  SPComplexTerm (SPCustomSymbol cst :: SPIdentifier
cst) [] | SPIdentifier -> Bool
isVar SPIdentifier
cst -> case SPIdentifier -> RMap -> Maybe (CType, Maybe Id)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SPIdentifier
cst RMap
m of
    Just (CVar s :: Id
s, _) -> VAR_DECL -> m VAR_DECL
forall (m :: * -> *) a. Monad m => a -> m a
return (VAR_DECL -> m VAR_DECL) -> VAR_DECL -> m VAR_DECL
forall a b. (a -> b) -> a -> b
$ [SPIdentifier] -> Id -> Range -> VAR_DECL
Var_decl [SPIdentifier
cst] Id
s Range
nullRange
    _ -> String -> m VAR_DECL
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m VAR_DECL) -> String -> m VAR_DECL
forall a b. (a -> b) -> a -> b
$ "unknown variable: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPIdentifier -> String
forall a. Show a => a -> String
show SPIdentifier
cst
  _ -> String -> m VAR_DECL
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m VAR_DECL) -> String -> m VAR_DECL
forall a b. (a -> b) -> a -> b
$ "quantified term as variable: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPTerm -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SPTerm
sp ""

isVar :: SPIdentifier -> Bool
isVar :: SPIdentifier -> Bool
isVar cst :: SPIdentifier
cst = case SPIdentifier -> String
tokStr SPIdentifier
cst of
    c :: Char
c : _ -> Char -> Bool
isUpper Char
c
    "" -> String -> Bool
forall a. (?callStack::CallStack) => String -> a
error "isVar"

getVars :: SPTerm -> [SPIdentifier]
getVars :: SPTerm -> [SPIdentifier]
getVars tm :: SPTerm
tm = case SPTerm
tm of
    SPComplexTerm (SPCustomSymbol cst :: SPIdentifier
cst) args :: [SPTerm]
args ->
        if [SPTerm] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SPTerm]
args then [SPIdentifier
cst] else (SPTerm -> [SPIdentifier]) -> [SPTerm] -> [SPIdentifier]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SPTerm -> [SPIdentifier]
getVars [SPTerm]
args
    _ -> []