{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/SoftFOL2CommonLogic.hs
Description :  Coding of SoftFOL into CommonLogic
Copyright   :  (c) Eugen Kuksa and Uni Bremen 2011
License     :  GPLv2 or higher, see LICENSE.txt

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

The translating comorphism from SoftFOL to CommonLogic.
-}

module Comorphisms.SoftFOL2CommonLogic
    (
     SoftFOL2CommonLogic (..)
    )
    where

import Data.Maybe (maybeToList)

import Common.ProofTree
import Common.Id
import Common.Result
import Common.Utils (concatMapM)
import qualified Common.AS_Annotation as AS_Anno
import qualified Common.DefaultMorphism as DefaultMorphism
import qualified Common.Lib.Rel as Rel
import qualified Control.Monad.Fail as Fail

import Logic.Logic
import Logic.Comorphism

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

-- SoftFOL
import qualified SoftFOL.Logic_SoftFOL as FOLLogic
import qualified SoftFOL.Sign as FOLSign

-- CommonLogic
import CommonLogic.AS_CommonLogic
import qualified CommonLogic.Logic_CommonLogic as ClLogic
import qualified CommonLogic.Sign as ClSign
import qualified CommonLogic.Symbol as ClSymbol
import qualified CommonLogic.Morphism as ClMor
import qualified CommonLogic.Sublogic as ClSL

-- | lid of the morphism
data SoftFOL2CommonLogic = SoftFOL2CommonLogic deriving Int -> SoftFOL2CommonLogic -> ShowS
[SoftFOL2CommonLogic] -> ShowS
SoftFOL2CommonLogic -> String
(Int -> SoftFOL2CommonLogic -> ShowS)
-> (SoftFOL2CommonLogic -> String)
-> ([SoftFOL2CommonLogic] -> ShowS)
-> Show SoftFOL2CommonLogic
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SoftFOL2CommonLogic] -> ShowS
$cshowList :: [SoftFOL2CommonLogic] -> ShowS
show :: SoftFOL2CommonLogic -> String
$cshow :: SoftFOL2CommonLogic -> String
showsPrec :: Int -> SoftFOL2CommonLogic -> ShowS
$cshowsPrec :: Int -> SoftFOL2CommonLogic -> ShowS
Show

instance Language SoftFOL2CommonLogic where
  language_name :: SoftFOL2CommonLogic -> String
language_name SoftFOL2CommonLogic = "SoftFOL2CommonLogic"

instance Comorphism SoftFOL2CommonLogic
    FOLLogic.SoftFOL         -- lid domain
    ()                       -- sublogics codomain
    [FOLSign.TPTP]          -- Basic spec domain
    FOLSign.Sentence         -- sentence domain
    ()                       -- symbol items domain
    ()                       -- symbol map items domain
    FOLSign.Sign             -- signature domain
    FOLSign.SoftFOLMorphism  -- morphism domain
    FOLSign.SFSymbol         -- symbol domain
    ()                       -- rawsymbol domain
    ProofTree                -- proof tree codomain
    ClLogic.CommonLogic      -- lid domain
    ClSL.CommonLogicSL       -- sublogics codomain
    BASIC_SPEC               -- Basic spec domain
    TEXT_META                -- sentence domain
    SYMB_ITEMS               -- symb_items
    SYMB_MAP_ITEMS           -- symbol map items domain
    ClSign.Sign              -- signature domain
    ClMor.Morphism           -- morphism domain
    ClSymbol.Symbol          -- symbol domain
    ClSymbol.Symbol          -- rawsymbol domain
    ProofTree                -- proof tree codomain
    where
      sourceLogic :: SoftFOL2CommonLogic -> SoftFOL
sourceLogic SoftFOL2CommonLogic = SoftFOL
FOLLogic.SoftFOL
      sourceSublogic :: SoftFOL2CommonLogic -> ()
sourceSublogic SoftFOL2CommonLogic = ()
      targetLogic :: SoftFOL2CommonLogic -> CommonLogic
targetLogic SoftFOL2CommonLogic = CommonLogic
ClLogic.CommonLogic
      mapSublogic :: SoftFOL2CommonLogic -> () -> Maybe CommonLogicSL
mapSublogic SoftFOL2CommonLogic = CommonLogicSL -> Maybe CommonLogicSL
forall a. a -> Maybe a
Just (CommonLogicSL -> Maybe CommonLogicSL)
-> (() -> CommonLogicSL) -> () -> Maybe CommonLogicSL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> CommonLogicSL
mapSub
      map_theory :: SoftFOL2CommonLogic
-> (Sign, [Named Sentence]) -> Result (Sign, [Named TEXT_META])
map_theory SoftFOL2CommonLogic = (Sign, [Named Sentence]) -> Result (Sign, [Named TEXT_META])
mapTheory
      map_sentence :: SoftFOL2CommonLogic -> Sign -> Sentence -> Result TEXT_META
map_sentence SoftFOL2CommonLogic = Sign -> Sentence -> Result TEXT_META
mapSentence
      map_morphism :: SoftFOL2CommonLogic -> SoftFOLMorphism -> Result Morphism
map_morphism SoftFOL2CommonLogic = SoftFOLMorphism -> Result Morphism
mapMor

mapSub :: () -> ClSL.CommonLogicSL
mapSub :: () -> CommonLogicSL
mapSub _ = CommonLogicSL
ClSL.folsl

mapMor :: FOLSign.SoftFOLMorphism -> Result ClMor.Morphism
mapMor :: SoftFOLMorphism -> Result Morphism
mapMor mor :: SoftFOLMorphism
mor =
  let src :: Sign
src = Sign -> Sign
mapSign (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ SoftFOLMorphism -> Sign
forall sign. DefaultMorphism sign -> sign
DefaultMorphism.domOfDefaultMorphism SoftFOLMorphism
mor
      tgt :: Sign
tgt = Sign -> Sign
mapSign (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ SoftFOLMorphism -> Sign
forall sign. DefaultMorphism sign -> sign
DefaultMorphism.codOfDefaultMorphism SoftFOLMorphism
mor
      pmp :: Map k a
pmp = Map k a
forall k a. Map k a
Map.empty
  in Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism -> Result Morphism) -> Morphism -> Result Morphism
forall a b. (a -> b) -> a -> b
$ Sign -> Sign -> Map Id Id -> Morphism
ClMor.Morphism Sign
src Sign
tgt Map Id Id
forall k a. Map k a
pmp

mapSentence :: FOLSign.Sign -> FOLSign.Sentence -> Result TEXT_META
mapSentence :: Sign -> Sentence -> Result TEXT_META
mapSentence = Sign -> Sentence -> Result TEXT_META
translate

mapSign :: FOLSign.Sign -> ClSign.Sign
mapSign :: Sign -> Sign
mapSign sig :: Sign
sig =
  let items :: Set Id
items = (Token -> Id) -> Set Token -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ t :: Token
t -> [Token] -> Id
mkId [Token
t]) (Set Token -> Set Id) -> Set Token -> Set Id
forall a b. (a -> b) -> a -> b
$ [Token] -> Set Token
forall a. Ord a => [a] -> Set a
Set.fromList ([Token] -> Set Token) -> [Token] -> Set Token
forall a b. (a -> b) -> a -> b
$ [[Token]] -> [Token]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
                                [ Map Token (Maybe Generated) -> [Token]
forall k a. Map k a -> [k]
Map.keys (Map Token (Maybe Generated) -> [Token])
-> Map Token (Maybe Generated) -> [Token]
forall a b. (a -> b) -> a -> b
$ Sign -> Map Token (Maybe Generated)
FOLSign.sortMap Sign
sig
                                , Map Token (Set ([Token], Token)) -> [Token]
forall k a. Map k a -> [k]
Map.keys (Map Token (Set ([Token], Token)) -> [Token])
-> Map Token (Set ([Token], Token)) -> [Token]
forall a b. (a -> b) -> a -> b
$ Sign -> Map Token (Set ([Token], Token))
FOLSign.funcMap Sign
sig
                                , Map Token (Set [Token]) -> [Token]
forall k a. Map k a -> [k]
Map.keys (Map Token (Set [Token]) -> [Token])
-> Map Token (Set [Token]) -> [Token]
forall a b. (a -> b) -> a -> b
$ Sign -> Map Token (Set [Token])
FOLSign.predMap Sign
sig
                                ]
  in Sign
ClSign.emptySig { discourseNames :: Set Id
ClSign.discourseNames = Set Id
items }

-- | translates SoftFOL-theories to CL-theories keeping their names
mapTheory :: (FOLSign.Sign, [AS_Anno.Named FOLSign.Sentence])
             -> Result (ClSign.Sign, [AS_Anno.Named TEXT_META])
mapTheory :: (Sign, [Named Sentence]) -> Result (Sign, [Named TEXT_META])
mapTheory (srcSign :: Sign
srcSign, srcFormulas :: [Named Sentence]
srcFormulas) = do
  [(String, TEXT_META)]
trans_fs <- (Named Sentence -> Result (String, TEXT_META))
-> [Named Sentence] -> Result [(String, TEXT_META)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((String, Sentence) -> Result (String, TEXT_META)
transSnd ((String, Sentence) -> Result (String, TEXT_META))
-> (Named Sentence -> (String, Sentence))
-> Named Sentence
-> Result (String, TEXT_META)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named Sentence -> (String, Sentence)
senAndName) [Named Sentence]
srcFormulas
  (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign -> Sign
mapSign Sign
srcSign, Sign -> [Named TEXT_META]
signToTexts Sign
srcSign
       [Named TEXT_META] -> [Named TEXT_META] -> [Named TEXT_META]
forall a. [a] -> [a] -> [a]
++ ((String, TEXT_META) -> Named TEXT_META)
-> [(String, TEXT_META)] -> [Named TEXT_META]
forall a b. (a -> b) -> [a] -> [b]
map ((String -> TEXT_META -> Named TEXT_META)
-> (String, TEXT_META) -> Named TEXT_META
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry String -> TEXT_META -> Named TEXT_META
forall a s. a -> s -> SenAttr s a
AS_Anno.makeNamed) [(String, TEXT_META)]
trans_fs)
  where senAndName :: AS_Anno.Named FOLSign.Sentence -> (String, FOLSign.Sentence)
        senAndName :: Named Sentence -> (String, Sentence)
senAndName f :: Named Sentence
f = (Named Sentence -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named Sentence
f, Named Sentence -> Sentence
forall s a. SenAttr s a -> s
AS_Anno.sentence Named Sentence
f)
        transSnd :: (String, FOLSign.Sentence) -> Result (String, TEXT_META)
        transSnd :: (String, Sentence) -> Result (String, TEXT_META)
transSnd (s :: String
s, f :: Sentence
f) = do
          TEXT_META
tm <- Sign -> Sentence -> Result TEXT_META
translate Sign
srcSign Sentence
f
          (String, TEXT_META) -> Result (String, TEXT_META)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
s, TEXT_META
tm)

-- translates a SoftFOL-theory to a CL-Text
translate :: FOLSign.Sign -> FOLSign.Sentence -> Result TEXT_META
translate :: Sign -> Sentence -> Result TEXT_META
translate s :: Sign
s f :: Sentence
f = do
  SENTENCE
sen <- Sign -> Sentence -> Result SENTENCE
trmToSen Sign
s Sentence
f
  TEXT_META -> Result TEXT_META
forall (m :: * -> *) a. Monad m => a -> m a
return (TEXT_META -> Result TEXT_META) -> TEXT_META -> Result TEXT_META
forall a b. (a -> b) -> a -> b
$ TEXT_META
emptyTextMeta { getText :: TEXT
getText = [PHRASE] -> Range -> TEXT
Text [SENTENCE -> PHRASE
Sentence SENTENCE
sen] Range
nullRange }

signToTexts :: FOLSign.Sign -> [AS_Anno.Named TEXT_META]
signToTexts :: Sign -> [Named TEXT_META]
signToTexts srcSign :: Sign
srcSign =
  let sr :: Maybe TEXT_META
sr = Map Token (Set Token) -> Maybe TEXT_META
sortRelText (Map Token (Set Token) -> Maybe TEXT_META)
-> Map Token (Set Token) -> Maybe TEXT_META
forall a b. (a -> b) -> a -> b
$ Rel Token -> Map Token (Set Token)
forall a. Rel a -> Map a (Set a)
Rel.toMap (Rel Token -> Map Token (Set Token))
-> Rel Token -> Map Token (Set Token)
forall a b. (a -> b) -> a -> b
$ Sign -> Rel Token
FOLSign.sortRel Sign
srcSign
      fm :: Maybe TEXT_META
fm = Map Token (Set ([Token], Token)) -> Maybe TEXT_META
funcMapText (Map Token (Set ([Token], Token)) -> Maybe TEXT_META)
-> Map Token (Set ([Token], Token)) -> Maybe TEXT_META
forall a b. (a -> b) -> a -> b
$ Sign -> Map Token (Set ([Token], Token))
FOLSign.funcMap Sign
srcSign
      pm :: Maybe TEXT_META
pm = Map Token (Set [Token]) -> Maybe TEXT_META
predMapText (Map Token (Set [Token]) -> Maybe TEXT_META)
-> Map Token (Set [Token]) -> Maybe TEXT_META
forall a b. (a -> b) -> a -> b
$ Sign -> Map Token (Set [Token])
FOLSign.predMap Sign
srcSign
  in [[Named TEXT_META]] -> [Named TEXT_META]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ (TEXT_META -> Named TEXT_META) -> [TEXT_META] -> [Named TEXT_META]
forall a b. (a -> b) -> [a] -> [b]
map (String -> TEXT_META -> Named TEXT_META
forall a s. a -> s -> SenAttr s a
AS_Anno.makeNamed String
sortRelTrS) (Maybe TEXT_META -> [TEXT_META]
forall a. Maybe a -> [a]
maybeToList Maybe TEXT_META
sr)
      , (TEXT_META -> Named TEXT_META) -> [TEXT_META] -> [Named TEXT_META]
forall a b. (a -> b) -> [a] -> [b]
map (String -> TEXT_META -> Named TEXT_META
forall a s. a -> s -> SenAttr s a
AS_Anno.makeNamed String
funcMapTrS) (Maybe TEXT_META -> [TEXT_META]
forall a. Maybe a -> [a]
maybeToList Maybe TEXT_META
fm)
      , (TEXT_META -> Named TEXT_META) -> [TEXT_META] -> [Named TEXT_META]
forall a b. (a -> b) -> [a] -> [b]
map (String -> TEXT_META -> Named TEXT_META
forall a s. a -> s -> SenAttr s a
AS_Anno.makeNamed String
predMapTrS) (Maybe TEXT_META -> [TEXT_META]
forall a. Maybe a -> [a]
maybeToList Maybe TEXT_META
pm)
      ]

-- creates one-sentence-phrases: forall x. (subSort x) => (superSort x)
sortRelText :: Map.Map FOLSign.SPIdentifier (Set.Set FOLSign.SPIdentifier)
                -> Maybe TEXT_META
sortRelText :: Map Token (Set Token) -> Maybe TEXT_META
sortRelText m :: Map Token (Set Token)
m =
  let ps :: [PHRASE]
ps = (Token -> Set Token -> [PHRASE] -> [PHRASE])
-> [PHRASE] -> Map Token (Set Token) -> [PHRASE]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ subSrt :: Token
subSrt set :: Set Token
set phrs :: [PHRASE]
phrs ->
        (Token -> [PHRASE] -> [PHRASE])
-> [PHRASE] -> Set Token -> [PHRASE]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ superSrt :: Token
superSrt phrs2 :: [PHRASE]
phrs2 ->
            SENTENCE -> PHRASE
Sentence (QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
Quant_sent QUANT
Universal [Token -> NAME_OR_SEQMARK
Name Token
xName]
                      (BOOL_SENT -> Range -> SENTENCE
Bool_sent (ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
BinOp ImplEq
Implication
                                  (Token -> [Token] -> SENTENCE
predicateNames Token
subSrt [Token
xName])
                                  (Token -> [Token] -> SENTENCE
predicateNames Token
superSrt [Token
xName])
                                 ) Range
nullRange) Range
nullRange)
            PHRASE -> [PHRASE] -> [PHRASE]
forall a. a -> [a] -> [a]
: [PHRASE]
phrs2) [] Set Token
set
        [PHRASE] -> [PHRASE] -> [PHRASE]
forall a. [a] -> [a] -> [a]
++ [PHRASE]
phrs) [] Map Token (Set Token)
m
  in if [PHRASE] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PHRASE]
ps
        then Maybe TEXT_META
forall a. Maybe a
Nothing
        else TEXT_META -> Maybe TEXT_META
forall a. a -> Maybe a
Just (TEXT_META -> Maybe TEXT_META) -> TEXT_META -> Maybe TEXT_META
forall a b. (a -> b) -> a -> b
$ TEXT_META
emptyTextMeta { getText :: TEXT
getText = Token -> TEXT -> Range -> TEXT
Named_text (String -> Token
mkSimpleId String
sortRelTrS)
                                                ([PHRASE] -> Range -> TEXT
Text [PHRASE]
ps Range
nullRange) Range
nullRange
                                  }

typesWithIndv :: [Token] -> [(Token, NAME)] -- (type, individual)
typesWithIndv :: [Token] -> [(Token, Token)]
typesWithIndv args :: [Token]
args =
  ((Token, Int) -> [(Token, Token)] -> [(Token, Token)])
-> [(Token, Token)] -> [(Token, Int)] -> [(Token, Token)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (a :: Token
a, i :: Int
i) resArg :: [(Token, Token)]
resArg -> (Token
a, Token -> Int -> Token
indv Token
a Int
i) (Token, Token) -> [(Token, Token)] -> [(Token, Token)]
forall a. a -> [a] -> [a]
: [(Token, Token)]
resArg) [] ([(Token, Int)] -> [(Token, Token)])
-> [(Token, Int)] -> [(Token, Token)]
forall a b. (a -> b) -> a -> b
$ [Token] -> [Int] -> [(Token, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Token]
args [0 ..]

{- creates one-sentence-phrases:
forall x y z. (if (and (T1 x) (T2 y) (T3 z)) (T4 f[x,y,z])) -}
funcMapText :: Map.Map Token (Set.Set ([Token], Token)) -> Maybe TEXT_META
funcMapText :: Map Token (Set ([Token], Token)) -> Maybe TEXT_META
funcMapText m :: Map Token (Set ([Token], Token))
m =
  let ps :: [PHRASE]
ps = (Token -> Set ([Token], Token) -> [PHRASE] -> [PHRASE])
-> [PHRASE] -> Map Token (Set ([Token], Token)) -> [PHRASE]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ f :: Token
f set :: Set ([Token], Token)
set phrs :: [PHRASE]
phrs ->
          (([Token], Token) -> [PHRASE] -> [PHRASE])
-> [PHRASE] -> Set ([Token], Token) -> [PHRASE]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ (args :: [Token]
args, res :: Token
res) phrs2 :: [PHRASE]
phrs2 ->
            let argsAndNames :: [(Token, Token)]
argsAndNames = [Token] -> [(Token, Token)]
typesWithIndv [Token]
args
            in SENTENCE -> PHRASE
Sentence (
                  if [Token] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Token]
args
                  then Token -> [Token] -> SENTENCE
predicateNames Token
res [Token
f]
                  else
                    QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
Quant_sent QUANT
Universal
                                (((Token, Token) -> NAME_OR_SEQMARK)
-> [(Token, Token)] -> [NAME_OR_SEQMARK]
forall a b. (a -> b) -> [a] -> [b]
map (Token -> NAME_OR_SEQMARK
Name (Token -> NAME_OR_SEQMARK)
-> ((Token, Token) -> Token) -> (Token, Token) -> NAME_OR_SEQMARK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Token, Token) -> Token
forall a b. (a, b) -> b
snd) [(Token, Token)]
argsAndNames) (
                      BOOL_SENT -> Range -> SENTENCE
Bool_sent (ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
BinOp ImplEq
Implication
                          (BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction ([SENTENCE] -> BOOL_SENT) -> [SENTENCE] -> BOOL_SENT
forall a b. (a -> b) -> a -> b
$
                              ((Token, Token) -> SENTENCE) -> [(Token, Token)] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (\ (p :: Token
p, x :: Token
x) -> Token -> [Token] -> SENTENCE
predicateNames Token
p [Token
x]) [(Token, Token)]
argsAndNames
                            ) Range
nullRange)
                          (ATOM -> Range -> SENTENCE
Atom_sent (TERM -> [TERM_SEQ] -> ATOM
Atom
                              (Token -> TERM
Name_term Token
res)
                              [TERM -> TERM_SEQ
Term_seq (TERM -> TERM_SEQ) -> TERM -> TERM_SEQ
forall a b. (a -> b) -> a -> b
$ TERM -> [TERM_SEQ] -> Range -> TERM
Funct_term (Token -> TERM
Name_term Token
f) (
                                  ((Token, Token) -> TERM_SEQ) -> [(Token, Token)] -> [TERM_SEQ]
forall a b. (a -> b) -> [a] -> [b]
map (TERM -> TERM_SEQ
Term_seq (TERM -> TERM_SEQ)
-> ((Token, Token) -> TERM) -> (Token, Token) -> TERM_SEQ
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> TERM
Name_term (Token -> TERM)
-> ((Token, Token) -> Token) -> (Token, Token) -> TERM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Token, Token) -> Token
forall a b. (a, b) -> b
snd) [(Token, Token)]
argsAndNames
                                ) Range
nullRange]
                            ) Range
nullRange)
                        ) Range
nullRange
                      ) Range
nullRange)
            PHRASE -> [PHRASE] -> [PHRASE]
forall a. a -> [a] -> [a]
: [PHRASE]
phrs2) [] Set ([Token], Token)
set
          [PHRASE] -> [PHRASE] -> [PHRASE]
forall a. [a] -> [a] -> [a]
++ [PHRASE]
phrs) [] Map Token (Set ([Token], Token))
m
  in if [PHRASE] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PHRASE]
ps
        then Maybe TEXT_META
forall a. Maybe a
Nothing
        else TEXT_META -> Maybe TEXT_META
forall a. a -> Maybe a
Just (TEXT_META -> Maybe TEXT_META) -> TEXT_META -> Maybe TEXT_META
forall a b. (a -> b) -> a -> b
$ TEXT_META
emptyTextMeta { getText :: TEXT
getText = Token -> TEXT -> Range -> TEXT
Named_text (String -> Token
mkSimpleId String
funcMapTrS)
                                                ([PHRASE] -> Range -> TEXT
Text [PHRASE]
ps Range
nullRange) Range
nullRange
                                  }

{- creates one-sentence-phrases:
forall x y z. (P[x,y,z]) => (and (T1 x) (T2 y) (T3 z)) -}
predMapText :: Map.Map Token (Set.Set [Token]) -> Maybe TEXT_META
predMapText :: Map Token (Set [Token]) -> Maybe TEXT_META
predMapText m :: Map Token (Set [Token])
m =
  let ps :: [PHRASE]
ps = (Token -> Set [Token] -> [PHRASE] -> [PHRASE])
-> [PHRASE] -> Map Token (Set [Token]) -> [PHRASE]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ prd :: Token
prd set :: Set [Token]
set phrs :: [PHRASE]
phrs ->
          ([Token] -> [PHRASE] -> [PHRASE])
-> [PHRASE] -> Set [Token] -> [PHRASE]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ args :: [Token]
args phrs2 :: [PHRASE]
phrs2 ->
            let argsAndNames :: [(Token, Token)]
argsAndNames = [Token] -> [(Token, Token)]
typesWithIndv [Token]
args
            in SENTENCE -> PHRASE
Sentence (QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
Quant_sent QUANT
Universal
                                      (((Token, Token) -> NAME_OR_SEQMARK)
-> [(Token, Token)] -> [NAME_OR_SEQMARK]
forall a b. (a -> b) -> [a] -> [b]
map (Token -> NAME_OR_SEQMARK
Name (Token -> NAME_OR_SEQMARK)
-> ((Token, Token) -> Token) -> (Token, Token) -> NAME_OR_SEQMARK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Token, Token) -> Token
forall a b. (a, b) -> b
snd) [(Token, Token)]
argsAndNames) (
                    BOOL_SENT -> Range -> SENTENCE
Bool_sent (ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
BinOp ImplEq
Implication
                        (Token -> [Token] -> SENTENCE
predicateNames Token
prd (((Token, Token) -> Token) -> [(Token, Token)] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map (Token, Token) -> Token
forall a b. (a, b) -> b
snd [(Token, Token)]
argsAndNames))
                        (BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction ([SENTENCE] -> BOOL_SENT) -> [SENTENCE] -> BOOL_SENT
forall a b. (a -> b) -> a -> b
$
                            ((Token, Token) -> SENTENCE) -> [(Token, Token)] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (\ (p :: Token
p, x :: Token
x) -> Token -> [Token] -> SENTENCE
predicateNames Token
p [Token
x]) [(Token, Token)]
argsAndNames
                          ) Range
nullRange)
                      ) Range
nullRange
                    ) Range
nullRange)
            PHRASE -> [PHRASE] -> [PHRASE]
forall a. a -> [a] -> [a]
: [PHRASE]
phrs2) [] Set [Token]
set
          [PHRASE] -> [PHRASE] -> [PHRASE]
forall a. [a] -> [a] -> [a]
++ [PHRASE]
phrs) [] Map Token (Set [Token])
m
  in if [PHRASE] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PHRASE]
ps
        then Maybe TEXT_META
forall a. Maybe a
Nothing
        else TEXT_META -> Maybe TEXT_META
forall a. a -> Maybe a
Just (TEXT_META -> Maybe TEXT_META) -> TEXT_META -> Maybe TEXT_META
forall a b. (a -> b) -> a -> b
$ TEXT_META
emptyTextMeta { getText :: TEXT
getText = Token -> TEXT -> Range -> TEXT
Named_text
                                                (String -> Token
mkSimpleId String
predMapTrS)
                                                ([PHRASE] -> Range -> TEXT
Text [PHRASE]
ps Range
nullRange)
                                                Range
nullRange
                                  }

trmToSen :: FOLSign.Sign -> FOLSign.SPTerm -> Result SENTENCE
trmToSen :: Sign -> Sentence -> Result SENTENCE
trmToSen s :: Sign
s t :: Sentence
t = case Sentence
t of
  FOLSign.SPQuantTerm qsym :: SPQuantSym
qsym vl :: [Sentence]
vl f :: Sentence
f -> Sign -> SPQuantSym -> [Sentence] -> Sentence -> Result SENTENCE
quantTrm Sign
s SPQuantSym
qsym [Sentence]
vl Sentence
f
  FOLSign.SPComplexTerm sym :: SPSymbol
sym args :: [Sentence]
args -> case SPSymbol
sym of
    FOLSign.SPEqual -> case [Sentence]
args of
        [x :: Sentence
x, y :: Sentence
y] -> (Sentence, Sentence) -> Result SENTENCE
toEquation (Sentence
x, Sentence
y)
        l :: [Sentence]
l@(_ : _ : _) -> do
            [SENTENCE]
eqs <- ((Sentence, Sentence) -> Result SENTENCE)
-> [(Sentence, Sentence)] -> Result [SENTENCE]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sentence, Sentence) -> Result SENTENCE
toEquation ([(Sentence, Sentence)] -> Result [SENTENCE])
-> [(Sentence, Sentence)] -> Result [SENTENCE]
forall a b. (a -> b) -> a -> b
$ [Sentence] -> [Sentence] -> [(Sentence, Sentence)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Sentence]
l ([Sentence] -> [(Sentence, Sentence)])
-> [Sentence] -> [(Sentence, Sentence)]
forall a b. (a -> b) -> a -> b
$ [Sentence] -> [Sentence]
forall a. [a] -> [a]
tail [Sentence]
l
            SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction [SENTENCE]
eqs) Range
nullRange
        x :: [Sentence]
x -> String -> Result SENTENCE
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result SENTENCE) -> String -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ "equation needs at least two arguments, but found: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Sentence] -> String
forall a. Show a => a -> String
show [Sentence]
x
    FOLSign.SPTrue -> SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return SENTENCE
clTrue
    FOLSign.SPFalse -> SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return SENTENCE
clFalse
    FOLSign.SPOr -> do
        [SENTENCE]
sens <- (Sentence -> Result SENTENCE) -> [Sentence] -> Result [SENTENCE]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sign -> Sentence -> Result SENTENCE
trmToSen Sign
s) [Sentence]
args
        SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Disjunction [SENTENCE]
sens) Range
nullRange
    FOLSign.SPAnd -> do
        [SENTENCE]
sens <- (Sentence -> Result SENTENCE) -> [Sentence] -> Result [SENTENCE]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sign -> Sentence -> Result SENTENCE
trmToSen Sign
s) [Sentence]
args
        SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction [SENTENCE]
sens) Range
nullRange
    FOLSign.SPNot -> case [Sentence]
args of
        [x :: Sentence
x] -> do
          SENTENCE
sen <- Sign -> Sentence -> Result SENTENCE
trmToSen Sign
s Sentence
x
          SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ BOOL_SENT -> Range -> SENTENCE
Bool_sent (SENTENCE -> BOOL_SENT
Negation SENTENCE
sen) Range
nullRange
        _ -> String -> Result SENTENCE
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result SENTENCE) -> String -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$
              "negation can only be applied to a single argument, but found: "
              String -> ShowS
forall a. [a] -> [a] -> [a]
++ Sentence -> String
forall a. Show a => a -> String
show Sentence
t
    FOLSign.SPImplies -> case [Sentence]
args of
        [x :: Sentence
x, y :: Sentence
y] -> do
            SENTENCE
sen1 <- Sign -> Sentence -> Result SENTENCE
trmToSen Sign
s Sentence
x
            SENTENCE
sen2 <- Sign -> Sentence -> Result SENTENCE
trmToSen Sign
s Sentence
y
            SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ BOOL_SENT -> Range -> SENTENCE
Bool_sent (ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
BinOp ImplEq
Implication SENTENCE
sen1 SENTENCE
sen2) Range
nullRange
        _ -> String -> Result SENTENCE
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result SENTENCE) -> String -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$
              "implication can only be applied to two arguments, but found: "
              String -> ShowS
forall a. [a] -> [a] -> [a]
++ Sentence -> String
forall a. Show a => a -> String
show Sentence
t
    FOLSign.SPImplied -> case [Sentence]
args of
        [x :: Sentence
x, y :: Sentence
y] -> do
            SENTENCE
sen1 <- Sign -> Sentence -> Result SENTENCE
trmToSen Sign
s Sentence
x
            SENTENCE
sen2 <- Sign -> Sentence -> Result SENTENCE
trmToSen Sign
s Sentence
y
            SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ BOOL_SENT -> Range -> SENTENCE
Bool_sent (ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
BinOp ImplEq
Implication SENTENCE
sen2 SENTENCE
sen1) Range
nullRange
        _ -> String -> Result SENTENCE
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result SENTENCE) -> String -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$
              "implication can only be applied to two arguments, but found: "
              String -> ShowS
forall a. [a] -> [a] -> [a]
++ Sentence -> String
forall a. Show a => a -> String
show Sentence
t
    FOLSign.SPEquiv -> case [Sentence]
args of
        [x :: Sentence
x, y :: Sentence
y] -> do
            SENTENCE
sen1 <- Sign -> Sentence -> Result SENTENCE
trmToSen Sign
s Sentence
x
            SENTENCE
sen2 <- Sign -> Sentence -> Result SENTENCE
trmToSen Sign
s Sentence
y
            SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ BOOL_SENT -> Range -> SENTENCE
Bool_sent (ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
BinOp ImplEq
Biconditional SENTENCE
sen1 SENTENCE
sen2) Range
nullRange
        _ -> String -> Result SENTENCE
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result SENTENCE) -> String -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$
              "equivalence can only be applied to two arguments, but found: "
              String -> ShowS
forall a. [a] -> [a] -> [a]
++ Sentence -> String
forall a. Show a => a -> String
show Sentence
t
    _ -> TERM -> [Sentence] -> Result SENTENCE
predicateSPTerms (SPSymbol -> TERM
symToTerm SPSymbol
sym) [Sentence]
args

-- | converts SPEquation to a CL-Equation
toEquation :: (FOLSign.SPTerm, FOLSign.SPTerm) -> Result SENTENCE
toEquation :: (Sentence, Sentence) -> Result SENTENCE
toEquation (x :: Sentence
x, y :: Sentence
y) = do
  TERM
trmx <- Sentence -> Result TERM
trmToTerm Sentence
x
  TERM
trmy <- Sentence -> Result TERM
trmToTerm Sentence
y
  SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ ATOM -> Range -> SENTENCE
Atom_sent (TERM -> TERM -> ATOM
Equation TERM
trmx TERM
trmy) Range
nullRange

predicateSPTerms :: TERM -> [FOLSign.SPTerm] -> Result SENTENCE
predicateSPTerms :: TERM -> [Sentence] -> Result SENTENCE
predicateSPTerms t :: TERM
t args :: [Sentence]
args = do
  [TERM_SEQ]
tseqs <- (Sentence -> Result TERM_SEQ) -> [Sentence] -> Result [TERM_SEQ]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Sentence -> Result TERM_SEQ
trmToTermSeq [Sentence]
args
  SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ ATOM -> Range -> SENTENCE
Atom_sent (TERM -> [TERM_SEQ] -> ATOM
Atom TERM
t [TERM_SEQ]
tseqs) Range
nullRange

predicateNames :: NAME -> [NAME] -> SENTENCE
predicateNames :: Token -> [Token] -> SENTENCE
predicateNames p :: Token
p xs :: [Token]
xs =
  ATOM -> Range -> SENTENCE
Atom_sent (TERM -> [TERM_SEQ] -> ATOM
Atom (Token -> TERM
Name_term Token
p) ((Token -> TERM_SEQ) -> [Token] -> [TERM_SEQ]
forall a b. (a -> b) -> [a] -> [b]
map (TERM -> TERM_SEQ
Term_seq (TERM -> TERM_SEQ) -> (Token -> TERM) -> Token -> TERM_SEQ
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> TERM
Name_term) [Token]
xs)) Range
nullRange

predicateTerm :: NAME -> TERM -> SENTENCE
predicateTerm :: Token -> TERM -> SENTENCE
predicateTerm p :: Token
p xs :: TERM
xs = ATOM -> Range -> SENTENCE
Atom_sent (TERM -> [TERM_SEQ] -> ATOM
Atom (Token -> TERM
Name_term Token
p) [TERM -> TERM_SEQ
Term_seq TERM
xs]) Range
nullRange

{- Converts a quantified FOL-term to a CL-Quant_sent. Quantifier arguments
contain only the inner-most arguments  of the SoftFOL Quantifier in order to
convert sentences like
@forall s(Y1), t(u(Y2)) .  Y1 /= Y2@
to
@forall Y1, Y2 . S(Y1) & T(u(Y2)) & U(Y2) => Y1 /= Y2@
where S, T and U are the types that Y1, u(Y2) and Y2 must have
in order to apply functions/predicates s, t and u to them (defined in
funcMap and predMap). -}
quantTrm :: FOLSign.Sign -> FOLSign.SPQuantSym
            -> [FOLSign.SPTerm] -> FOLSign.SPTerm -> Result SENTENCE
quantTrm :: Sign -> SPQuantSym -> [Sentence] -> Sentence -> Result SENTENCE
quantTrm sig :: Sign
sig qsymm :: SPQuantSym
qsymm vs :: [Sentence]
vs f :: Sentence
f = do
  let functions_quant :: [Sentence]
functions_quant = (Sentence -> Bool) -> [Sentence] -> [Sentence]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Sentence -> Bool) -> Sentence -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sentence -> Bool
isNullary) [Sentence]
vs
  let trans_vs :: [NAME_OR_SEQMARK]
trans_vs = (Sentence -> [NAME_OR_SEQMARK]) -> [Sentence] -> [NAME_OR_SEQMARK]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Sentence -> [NAME_OR_SEQMARK]
trmToNameSeq [Sentence]
vs
  SENTENCE
trans_f <- if [Sentence] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Sentence]
functions_quant
             then Sign -> Sentence -> Result SENTENCE
trmToSen Sign
sig Sentence
f
             else do
               SENTENCE
sen1 <- Sign -> [Sentence] -> Result SENTENCE
typeSentence Sign
sig [Sentence]
functions_quant
               SENTENCE
sen2 <- Sign -> Sentence -> Result SENTENCE
trmToSen Sign
sig Sentence
f
               SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ BOOL_SENT -> Range -> SENTENCE
Bool_sent (ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
BinOp ImplEq
Implication SENTENCE
sen1 SENTENCE
sen2) Range
nullRange
  QUANT
quantifier <- case SPQuantSym
qsymm of
        FOLSign.SPForall -> QUANT -> Result QUANT
forall (m :: * -> *) a. Monad m => a -> m a
return QUANT
Universal
        FOLSign.SPExists -> QUANT -> Result QUANT
forall (m :: * -> *) a. Monad m => a -> m a
return QUANT
Existential
        _ -> String -> Result QUANT
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "custom quantifiers not allowed"
  SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
Quant_sent QUANT
quantifier [NAME_OR_SEQMARK]
trans_vs SENTENCE
trans_f Range
nullRange

typeSentence :: FOLSign.Sign -> [FOLSign.SPTerm] -> Result SENTENCE
typeSentence :: Sign -> [Sentence] -> Result SENTENCE
typeSentence sig :: Sign
sig vs :: [Sentence]
vs = case [Sentence]
vs of
  [] -> SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return SENTENCE
clTrue
  [v :: Sentence
v] -> Sign -> Sentence -> Result SENTENCE
typeSentence1 Sign
sig Sentence
v      -- v = f(x,y,z)
  _ -> do
      [SENTENCE]
sens <- (Sentence -> Result SENTENCE) -> [Sentence] -> Result [SENTENCE]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sign -> Sentence -> Result SENTENCE
typeSentence1 Sign
sig) [Sentence]
vs
      SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction [SENTENCE]
sens) Range
nullRange

typeSentence1 :: FOLSign.Sign -> FOLSign.SPTerm -> Result SENTENCE
typeSentence1 :: Sign -> Sentence -> Result SENTENCE
typeSentence1 sig :: Sign
sig v :: Sentence
v = case Sentence
v of
  FOLSign.SPComplexTerm _ [] ->
    String -> Result SENTENCE
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "bug (typeSentence1): nullary functions should not occur here"
  FOLSign.SPComplexTerm sym :: SPSymbol
sym args :: [Sentence]
args -> Sign -> Token -> [Sentence] -> Result SENTENCE
typeSentenceGetTypes Sign
sig (SPSymbol -> Token
symToName SPSymbol
sym) [Sentence]
args
  FOLSign.SPQuantTerm {} ->
    String -> Result SENTENCE
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "quantification not allowed in bound variable list"

typeSentenceGetTypes :: FOLSign.Sign -> FOLSign.SPIdentifier -> [FOLSign.SPTerm]
                        -> Result SENTENCE
typeSentenceGetTypes :: Sign -> Token -> [Sentence] -> Result SENTENCE
typeSentenceGetTypes sig :: Sign
sig symN :: Token
symN args :: [Sentence]
args =
  case Token
-> Map Token (Set ([Token], Token)) -> Maybe (Set ([Token], Token))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Token
symN (Map Token (Set ([Token], Token)) -> Maybe (Set ([Token], Token)))
-> Map Token (Set ([Token], Token)) -> Maybe (Set ([Token], Token))
forall a b. (a -> b) -> a -> b
$ Sign -> Map Token (Set ([Token], Token))
FOLSign.funcMap Sign
sig of
    Nothing -> case Token -> Map Token (Set [Token]) -> Maybe (Set [Token])
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Token
symN (Map Token (Set [Token]) -> Maybe (Set [Token]))
-> Map Token (Set [Token]) -> Maybe (Set [Token])
forall a b. (a -> b) -> a -> b
$ Sign -> Map Token (Set [Token])
FOLSign.predMap Sign
sig of
      Nothing -> case Token -> Map Token (Maybe Generated) -> Maybe (Maybe Generated)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Token
symN (Map Token (Maybe Generated) -> Maybe (Maybe Generated))
-> Map Token (Maybe Generated) -> Maybe (Maybe Generated)
forall a b. (a -> b) -> a -> b
$ Sign -> Map Token (Maybe Generated)
FOLSign.sortMap Sign
sig of
        Nothing -> String -> Result SENTENCE
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result SENTENCE) -> String -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ "symbol has no type: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
symN
        Just _ -> [Sentence] -> Token -> Result SENTENCE
typeSentencesSort [Sentence]
args Token
symN
      Just ts :: Set [Token]
ts -> Sign -> [Sentence] -> [[Token]] -> Result SENTENCE
typeSentencesDisjPred Sign
sig [Sentence]
args ([[Token]] -> Result SENTENCE) -> [[Token]] -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ Set [Token] -> [[Token]]
forall a. Set a -> [a]
Set.elems Set [Token]
ts
    Just ts :: Set ([Token], Token)
ts -> Sign -> [Sentence] -> [([Token], Token)] -> Result SENTENCE
typeSentencesDisjFunc Sign
sig [Sentence]
args ([([Token], Token)] -> Result SENTENCE)
-> [([Token], Token)] -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ Set ([Token], Token) -> [([Token], Token)]
forall a. Set a -> [a]
Set.elems Set ([Token], Token)
ts

typeSentencesSort :: [FOLSign.SPTerm] -> FOLSign.SPIdentifier
                     -> Result SENTENCE
typeSentencesSort :: [Sentence] -> Token -> Result SENTENCE
typeSentencesSort args :: [Sentence]
args srt :: Token
srt = case [Sentence]
args of
  [] -> String -> Result SENTENCE
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result SENTENCE) -> String -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ "no arguments for sort " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
srt
  [arg :: Sentence
arg] -> do
      TERM
funtrm <- Sentence -> Result TERM
trmToFunctTrm Sentence
arg
      SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ Token -> TERM -> SENTENCE
predicateTerm Token
srt TERM
funtrm
  _ -> do
      [SENTENCE]
sens <- (Sentence -> Result SENTENCE) -> [Sentence] -> Result [SENTENCE]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ arg :: Sentence
arg -> do
                     TERM
funtrm <- Sentence -> Result TERM
trmToFunctTrm Sentence
arg
                     SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ Token -> TERM -> SENTENCE
predicateTerm Token
srt TERM
funtrm
                   ) [Sentence]
args
      SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction [SENTENCE]
sens) Range
nullRange

typeSentencesDisjPred :: FOLSign.Sign -> [FOLSign.SPTerm]
                         -> [[FOLSign.SPIdentifier]]
                         -> Result SENTENCE
typeSentencesDisjPred :: Sign -> [Sentence] -> [[Token]] -> Result SENTENCE
typeSentencesDisjPred sig :: Sign
sig args :: [Sentence]
args typeSet :: [[Token]]
typeSet = case [[Token]]
typeSet of
  [t :: [Token]
t] -> [Token] -> Result SENTENCE
tsdp1 [Token]
t
  _ -> do
    [SENTENCE]
sens <- ([Token] -> Result SENTENCE) -> [[Token]] -> Result [SENTENCE]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM [Token] -> Result SENTENCE
tsdp1 [[Token]]
typeSet
    SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Disjunction [SENTENCE]
sens) Range
nullRange
  where tsdp1 :: [FOLSign.SPIdentifier] -> Result SENTENCE
        tsdp1 :: [Token] -> Result SENTENCE
tsdp1 t :: [Token]
t = do
          [SENTENCE]
sens <- ((Sentence, Token) -> Result SENTENCE)
-> [(Sentence, Token)] -> Result [SENTENCE]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (arg :: Sentence
arg, argType :: Token
argType) -> case Sentence
arg of
              FOLSign.SPComplexTerm _ [] ->
                SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> SENTENCE
predicateNames Token
argType [Sentence -> Token
trmToName Sentence
arg]
              FOLSign.SPComplexTerm _ _ ->
                Sign -> Sentence -> Result SENTENCE
typeSentence1 Sign
sig Sentence
arg
              FOLSign.SPQuantTerm {} ->
                String -> Result SENTENCE
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "quantification not allowed in quantifier-argument list"
            ) ([(Sentence, Token)] -> Result [SENTENCE])
-> [(Sentence, Token)] -> Result [SENTENCE]
forall a b. (a -> b) -> a -> b
$ [Sentence] -> [Token] -> [(Sentence, Token)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Sentence]
args [Token]
t
          SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction [SENTENCE]
sens) Range
nullRange

typeSentencesDisjFunc :: FOLSign.Sign -> [FOLSign.SPTerm]
                         -> [([FOLSign.SPIdentifier], FOLSign.SPIdentifier)]
                         -> Result SENTENCE
typeSentencesDisjFunc :: Sign -> [Sentence] -> [([Token], Token)] -> Result SENTENCE
typeSentencesDisjFunc sig :: Sign
sig args :: [Sentence]
args typeSet :: [([Token], Token)]
typeSet = case [([Token], Token)]
typeSet of
  [t :: ([Token], Token)
t] -> ([Token], Token) -> Result SENTENCE
tsdf1 ([Token], Token)
t
  _ -> do
      [SENTENCE]
sens <- (([Token], Token) -> Result SENTENCE)
-> [([Token], Token)] -> Result [SENTENCE]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Token], Token) -> Result SENTENCE
tsdf1 [([Token], Token)]
typeSet
      SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Disjunction [SENTENCE]
sens) Range
nullRange
  where tsdf1 :: ([FOLSign.SPIdentifier], FOLSign.SPIdentifier) -> Result SENTENCE
        tsdf1 :: ([Token], Token) -> Result SENTENCE
tsdf1 (t :: [Token]
t, resType :: Token
resType) = do
          [SENTENCE]
sens <- ((Sentence, Token) -> Result [SENTENCE])
-> [(Sentence, Token)] -> Result [SENTENCE]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m [b]) -> t a -> m [b]
concatMapM (\ (arg :: Sentence
arg, argType :: Token
argType) -> case Sentence
arg of
              FOLSign.SPComplexTerm _ [] ->
                [SENTENCE] -> Result [SENTENCE]
forall (m :: * -> *) a. Monad m => a -> m a
return [Token -> [Token] -> SENTENCE
predicateNames Token
argType [Sentence -> Token
trmToName Sentence
arg]]
              FOLSign.SPComplexTerm _ _ -> do
                TERM
funtrm <- Sentence -> Result TERM
trmToFunctTrm Sentence
arg
                SENTENCE
typsen <- Sign -> Sentence -> Result SENTENCE
typeSentence1 Sign
sig Sentence
arg
                [SENTENCE] -> Result [SENTENCE]
forall (m :: * -> *) a. Monad m => a -> m a
return [Token -> TERM -> SENTENCE
predicateTerm Token
resType TERM
funtrm, SENTENCE
typsen]
              FOLSign.SPQuantTerm {} ->
                String -> Result [SENTENCE]
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "quantification not allowed in quantifier-argument list"
            ) ([(Sentence, Token)] -> Result [SENTENCE])
-> [(Sentence, Token)] -> Result [SENTENCE]
forall a b. (a -> b) -> a -> b
$ [Sentence] -> [Token] -> [(Sentence, Token)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Sentence]
args [Token]
t
          SENTENCE -> Result SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> Result SENTENCE) -> SENTENCE -> Result SENTENCE
forall a b. (a -> b) -> a -> b
$ BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction [SENTENCE]
sens) Range
nullRange

trmToName :: FOLSign.SPTerm -> NAME
trmToName :: Sentence -> Token
trmToName t :: Sentence
t = case Sentence
t of
  FOLSign.SPComplexTerm sym :: SPSymbol
sym _ -> SPSymbol -> Token
symToName SPSymbol
sym
  x :: Sentence
x -> String -> Token
forall a. HasCallStack => String -> a
error (String -> Token) -> String -> Token
forall a b. (a -> b) -> a -> b
$ "quantification not convertible to a name: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Sentence -> String
forall a. Show a => a -> String
show Sentence
x

{- converts an @SPTerm@ to @[NAME_OR_SEQMARK]@ as an argument for a quantifier
using only the inner-most arguments -}
trmToNameSeq :: FOLSign.SPTerm -> [NAME_OR_SEQMARK]
trmToNameSeq :: Sentence -> [NAME_OR_SEQMARK]
trmToNameSeq t :: Sentence
t = case Sentence
t of
  FOLSign.SPComplexTerm sym :: SPSymbol
sym [] -> [Token -> NAME_OR_SEQMARK
Name (Token -> NAME_OR_SEQMARK) -> Token -> NAME_OR_SEQMARK
forall a b. (a -> b) -> a -> b
$ SPSymbol -> Token
symToName SPSymbol
sym]
  FOLSign.SPComplexTerm _ args :: [Sentence]
args -> (Sentence -> [NAME_OR_SEQMARK]) -> [Sentence] -> [NAME_OR_SEQMARK]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Sentence -> [NAME_OR_SEQMARK]
trmToNameSeq [Sentence]
args
  FOLSign.SPQuantTerm {} ->
      String -> [NAME_OR_SEQMARK]
forall a. HasCallStack => String -> a
error "quantification not allowed in quantifier-argument list"

-- converts an SPTerm to a TERM, i.e. for the arguments of an equation
trmToTerm :: FOLSign.SPTerm -> Result TERM
trmToTerm :: Sentence -> Result TERM
trmToTerm t :: Sentence
t = case Sentence
t of
  FOLSign.SPQuantTerm {} -> String -> Result TERM
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "quantification not allowed for a term"
  FOLSign.SPComplexTerm _ [] -> TERM -> Result TERM
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM -> Result TERM) -> TERM -> Result TERM
forall a b. (a -> b) -> a -> b
$ Token -> TERM
Name_term (Token -> TERM) -> Token -> TERM
forall a b. (a -> b) -> a -> b
$ Sentence -> Token
trmToName Sentence
t
  FOLSign.SPComplexTerm _ _ -> Sentence -> Result TERM
trmToFunctTrm Sentence
t

-- Converts an SPTerm to TERM_SEQ as an argument for a quantifier
trmToTermSeq :: FOLSign.SPTerm -> Result TERM_SEQ
trmToTermSeq :: Sentence -> Result TERM_SEQ
trmToTermSeq t :: Sentence
t = case Sentence
t of
  FOLSign.SPComplexTerm _ _ -> do
    TERM
tseq <- Sentence -> Result TERM
trmToTerm Sentence
t
    TERM_SEQ -> Result TERM_SEQ
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM_SEQ -> Result TERM_SEQ) -> TERM_SEQ -> Result TERM_SEQ
forall a b. (a -> b) -> a -> b
$ TERM -> TERM_SEQ
Term_seq TERM
tseq
  FOLSign.SPQuantTerm {} ->
      String -> Result TERM_SEQ
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "quantification not allowed in argument list"

trmToFunctTrm :: FOLSign.SPTerm -> Result TERM
trmToFunctTrm :: Sentence -> Result TERM
trmToFunctTrm t :: Sentence
t = case Sentence
t of
  FOLSign.SPComplexTerm sym :: SPSymbol
sym args :: [Sentence]
args ->
      if [Sentence] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Sentence]
args
      then TERM -> Result TERM
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM -> Result TERM) -> TERM -> Result TERM
forall a b. (a -> b) -> a -> b
$ SPSymbol -> TERM
symToTerm SPSymbol
sym
      else do
        [TERM_SEQ]
tseq <- (Sentence -> Result TERM_SEQ) -> [Sentence] -> Result [TERM_SEQ]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Sentence -> Result TERM_SEQ
trmToTermSeq [Sentence]
args
        TERM -> Result TERM
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM -> Result TERM) -> TERM -> Result TERM
forall a b. (a -> b) -> a -> b
$ TERM -> [TERM_SEQ] -> Range -> TERM
Funct_term (SPSymbol -> TERM
symToTerm SPSymbol
sym) [TERM_SEQ]
tseq Range
nullRange
  FOLSign.SPQuantTerm {} ->
      String -> Result TERM
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "quantification not allowed in quantifier-argument list"

-- | converts a custom symbol to a NAME, used in
symToName :: FOLSign.SPSymbol -> NAME
symToName :: SPSymbol -> Token
symToName s :: SPSymbol
s = case SPSymbol
s of
  FOLSign.SPCustomSymbol i :: Token
i -> Token
i
  FOLSign.SPID -> Token
idName
  FOLSign.SPDiv -> Token
divName
  FOLSign.SPComp -> Token
compName
  FOLSign.SPSum -> Token
sumName
  FOLSign.SPConv -> Token
convName
  x :: SPSymbol
x -> String -> Token
forall a. HasCallStack => String -> a
error (String -> Token) -> String -> Token
forall a b. (a -> b) -> a -> b
$ "symbol not convertible to a name: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SPSymbol -> String
forall a. Show a => a -> String
show SPSymbol
x

symToTerm :: FOLSign.SPSymbol -> TERM
symToTerm :: SPSymbol -> TERM
symToTerm s :: SPSymbol
s = Token -> TERM
Name_term (Token -> TERM) -> Token -> TERM
forall a b. (a -> b) -> a -> b
$ SPSymbol -> Token
symToName SPSymbol
s

isNullary :: FOLSign.SPTerm -> Bool
isNullary :: Sentence -> Bool
isNullary t :: Sentence
t = case Sentence
t of
  FOLSign.SPComplexTerm _ [] -> Bool
True
  _ -> Bool
False

-- representation for true in CL
clTrue :: SENTENCE -- forall x. x=x
clTrue :: SENTENCE
clTrue = QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
Quant_sent QUANT
Universal [Token -> NAME_OR_SEQMARK
Name Token
xName]
         (ATOM -> Range -> SENTENCE
Atom_sent (TERM -> TERM -> ATOM
Equation (Token -> TERM
Name_term Token
xName) (Token -> TERM
Name_term Token
xName)) Range
nullRange
         ) Range
nullRange

-- representation for false in CL
clFalse :: SENTENCE
clFalse :: SENTENCE
clFalse = BOOL_SENT -> Range -> SENTENCE
Bool_sent (SENTENCE -> BOOL_SENT
Negation SENTENCE
clTrue) Range
nullRange

-- creates an individual-name out of a NAME by appending "_i" to it
indv :: NAME -> Int -> NAME
indv :: Token -> Int -> Token
indv n :: Token
n i :: Int
i = String -> Token
mkSimpleId (Token -> String
tokStr Token
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_item_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)

-- simple names
xName :: NAME
xName :: Token
xName = String -> Token
mkSimpleId "x"

idName :: NAME
idName :: Token
idName = String -> Token
mkSimpleId "ID"

divName :: NAME
divName :: Token
divName = String -> Token
mkSimpleId "DIV"

compName :: NAME
compName :: Token
compName = String -> Token
mkSimpleId "COMP"

sumName :: NAME
sumName :: Token
sumName = String -> Token
mkSimpleId "SUM"

convName :: NAME
convName :: Token
convName = String -> Token
mkSimpleId "CONV"

-- Text-Names
sortRelTrS :: String
sortRelTrS :: String
sortRelTrS = "SoftFOL_SubsortRelations"

funcMapTrS :: String
funcMapTrS :: String
funcMapTrS = "SoftFOL_FunctionMaps"

predMapTrS :: String
predMapTrS :: String
predMapTrS = "SoftFOL_PredicateMaps"