{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/CommonLogic2CASL.hs
Description :  Comorphism from CommonLogic to CASL
Copyright   :  (c)  Eugen Kuksa, Uni Bremen 2011, DFKI GmbH 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (via Logic.Logic)

Translating comorphism from Common Logic
(with and without sequence markers) to CASL

-}

module Comorphisms.CommonLogic2CASL
  ( CL2CFOL (..)
  ) where

import Logic.Logic as Logic
import Logic.Comorphism

import Common.ProofTree
import Common.Token
import Common.Result
import Common.AS_Annotation as AS_Anno
import Common.Lib.MapSet (MapSet)
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel
import Common.Id

import Data.Function (on)
import qualified Data.Set as Set
import qualified Data.Map as Map

-- Common Logic
import qualified CommonLogic.Logic_CommonLogic as ClLogic
import qualified CommonLogic.AS_CommonLogic as Cl
import qualified CommonLogic.Sign as ClSign
import qualified CommonLogic.Symbol as ClSymbol
import qualified CommonLogic.Morphism as ClMor
import CommonLogic.Sublogic as ClSl
import CommonLogic.PredefinedCASLAxioms
import CommonLogic.ModuleElimination

-- CASL
import qualified CASL.Logic_CASL as CLogic
import CASL.AS_Basic_CASL as CBasic
import qualified CASL.Sublogic as CSL
import CASL.Sign as CSign
import CASL.Morphism as CMor

import qualified Control.Monad.Fail as Fail

newtype CL2CFOL = CL2CFOL { CL2CFOL -> CommonLogicSL
fol :: CommonLogicSL } deriving Int -> CL2CFOL -> ShowS
[CL2CFOL] -> ShowS
CL2CFOL -> String
(Int -> CL2CFOL -> ShowS)
-> (CL2CFOL -> String) -> ([CL2CFOL] -> ShowS) -> Show CL2CFOL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CL2CFOL] -> ShowS
$cshowList :: [CL2CFOL] -> ShowS
show :: CL2CFOL -> String
$cshow :: CL2CFOL -> String
showsPrec :: Int -> CL2CFOL -> ShowS
$cshowsPrec :: Int -> CL2CFOL -> ShowS
Show

showCLTextType :: Bool -> CLTextType -> String
showCLTextType :: Bool -> CLTextType -> String
showCLTextType b :: Bool
b s :: CLTextType
s = case CLTextType
s of
  FirstOrder -> if Bool
b then "Fol" else "Seq"
  Impredicative -> if Bool
b then "Imp" else "Full"
  _ -> CLTextType -> String
forall a. Show a => a -> String
show CLTextType
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ if Bool
b then "Compact" else ""

instance Language CL2CFOL where
  language_name :: CL2CFOL -> String
language_name (CL2CFOL b :: CommonLogicSL
b) = "CL"
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> CLTextType -> String
showCLTextType (CommonLogicSL -> Bool
compact CommonLogicSL
b) (CommonLogicSL -> CLTextType
format CommonLogicSL
b) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "2CFOL"

instance Comorphism
    CL2CFOL -- comorphism
    ClLogic.CommonLogic     -- lid domain
    ClSl.CommonLogicSL      -- sublogics codomain
    Cl.BASIC_SPEC           -- Basic spec domain
    Cl.TEXT_META            -- sentence domain
    Cl.SYMB_ITEMS           -- symbol items domain
    Cl.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
    CLogic.CASL             -- lid codomain
    CSL.CASL_Sublogics      -- sublogics codomain
    CLogic.CASLBasicSpec    -- Basic spec codomain
    CBasic.CASLFORMULA      -- sentence codomain
    CBasic.SYMB_ITEMS       -- symbol items codomain
    CBasic.SYMB_MAP_ITEMS   -- symbol map items codomain
    CSign.CASLSign          -- signature codomain
    CMor.CASLMor            -- morphism codomain
    CSign.Symbol            -- symbol codomain
    CMor.RawSymbol          -- rawsymbol codomain
    ProofTree               -- proof tree domain
    where
      sourceLogic :: CL2CFOL -> CommonLogic
sourceLogic (CL2CFOL _) = CommonLogic
ClLogic.CommonLogic
      sourceSublogic :: CL2CFOL -> CommonLogicSL
sourceSublogic (CL2CFOL b :: CommonLogicSL
b) = CommonLogicSL
b
      targetLogic :: CL2CFOL -> CASL
targetLogic (CL2CFOL _) = CASL
CLogic.CASL
      mapSublogic :: CL2CFOL -> CommonLogicSL -> Maybe CASL_Sublogics
mapSublogic (CL2CFOL _) = CASL_Sublogics -> Maybe CASL_Sublogics
forall a. a -> Maybe a
Just (CASL_Sublogics -> Maybe CASL_Sublogics)
-> (CommonLogicSL -> CASL_Sublogics)
-> CommonLogicSL
-> Maybe CASL_Sublogics
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommonLogicSL -> CASL_Sublogics
mapSub
      map_theory :: CL2CFOL
-> (Sign, [Named TEXT_META])
-> Result (CASLSign, [Named CASLFORMULA])
map_theory (CL2CFOL b :: CommonLogicSL
b) = CommonLogicSL
-> (Sign, [Named TEXT_META])
-> Result (CASLSign, [Named CASLFORMULA])
mapTheory CommonLogicSL
b
      map_morphism :: CL2CFOL -> Morphism -> Result CASLMor
map_morphism (CL2CFOL b :: CommonLogicSL
b) = CommonLogicSL -> Morphism -> Result CASLMor
mapMor CommonLogicSL
b
      map_sentence :: CL2CFOL -> Sign -> TEXT_META -> Result CASLFORMULA
map_sentence (CL2CFOL b :: CommonLogicSL
b) _ = CommonLogicSL -> TEXT_META -> Result CASLFORMULA
mapSentence CommonLogicSL
b
      has_model_expansion :: CL2CFOL -> Bool
has_model_expansion (CL2CFOL _) = Bool
True

data PredOrFunc = Pred | Func deriving (PredOrFunc -> PredOrFunc -> Bool
(PredOrFunc -> PredOrFunc -> Bool)
-> (PredOrFunc -> PredOrFunc -> Bool) -> Eq PredOrFunc
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PredOrFunc -> PredOrFunc -> Bool
$c/= :: PredOrFunc -> PredOrFunc -> Bool
== :: PredOrFunc -> PredOrFunc -> Bool
$c== :: PredOrFunc -> PredOrFunc -> Bool
Eq, Eq PredOrFunc
Eq PredOrFunc =>
(PredOrFunc -> PredOrFunc -> Ordering)
-> (PredOrFunc -> PredOrFunc -> Bool)
-> (PredOrFunc -> PredOrFunc -> Bool)
-> (PredOrFunc -> PredOrFunc -> Bool)
-> (PredOrFunc -> PredOrFunc -> Bool)
-> (PredOrFunc -> PredOrFunc -> PredOrFunc)
-> (PredOrFunc -> PredOrFunc -> PredOrFunc)
-> Ord PredOrFunc
PredOrFunc -> PredOrFunc -> Bool
PredOrFunc -> PredOrFunc -> Ordering
PredOrFunc -> PredOrFunc -> PredOrFunc
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 :: PredOrFunc -> PredOrFunc -> PredOrFunc
$cmin :: PredOrFunc -> PredOrFunc -> PredOrFunc
max :: PredOrFunc -> PredOrFunc -> PredOrFunc
$cmax :: PredOrFunc -> PredOrFunc -> PredOrFunc
>= :: PredOrFunc -> PredOrFunc -> Bool
$c>= :: PredOrFunc -> PredOrFunc -> Bool
> :: PredOrFunc -> PredOrFunc -> Bool
$c> :: PredOrFunc -> PredOrFunc -> Bool
<= :: PredOrFunc -> PredOrFunc -> Bool
$c<= :: PredOrFunc -> PredOrFunc -> Bool
< :: PredOrFunc -> PredOrFunc -> Bool
$c< :: PredOrFunc -> PredOrFunc -> Bool
compare :: PredOrFunc -> PredOrFunc -> Ordering
$ccompare :: PredOrFunc -> PredOrFunc -> Ordering
$cp1Ord :: Eq PredOrFunc
Ord, Int -> PredOrFunc -> ShowS
[PredOrFunc] -> ShowS
PredOrFunc -> String
(Int -> PredOrFunc -> ShowS)
-> (PredOrFunc -> String)
-> ([PredOrFunc] -> ShowS)
-> Show PredOrFunc
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PredOrFunc] -> ShowS
$cshowList :: [PredOrFunc] -> ShowS
show :: PredOrFunc -> String
$cshow :: PredOrFunc -> String
showsPrec :: Int -> PredOrFunc -> ShowS
$cshowsPrec :: Int -> PredOrFunc -> ShowS
Show)

data TextInfo = TextInfo
  { TextInfo -> MapSet String Int
arityPred :: MapSet String Int
  , TextInfo -> MapSet String Int
arityFunc :: MapSet String Int
  , TextInfo -> MapSet String Int
boundPred :: MapSet String Int
  , TextInfo -> MapSet String Int
boundFunc :: MapSet String Int
  , TextInfo -> Set String
seqMarkers :: Set.Set String
  } deriving Int -> TextInfo -> ShowS
[TextInfo] -> ShowS
TextInfo -> String
(Int -> TextInfo -> ShowS)
-> (TextInfo -> String) -> ([TextInfo] -> ShowS) -> Show TextInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TextInfo] -> ShowS
$cshowList :: [TextInfo] -> ShowS
show :: TextInfo -> String
$cshow :: TextInfo -> String
showsPrec :: Int -> TextInfo -> ShowS
$cshowsPrec :: Int -> TextInfo -> ShowS
Show

emptyTI :: TextInfo
emptyTI :: TextInfo
emptyTI = TextInfo :: MapSet String Int
-> MapSet String Int
-> MapSet String Int
-> MapSet String Int
-> Set String
-> TextInfo
TextInfo
  { arityPred :: MapSet String Int
arityPred = MapSet String Int
forall a b. MapSet a b
MapSet.empty
  , arityFunc :: MapSet String Int
arityFunc = MapSet String Int
forall a b. MapSet a b
MapSet.empty
  , boundPred :: MapSet String Int
boundPred = MapSet String Int
forall a b. MapSet a b
MapSet.empty
  , boundFunc :: MapSet String Int
boundFunc = MapSet String Int
forall a b. MapSet a b
MapSet.empty
  , seqMarkers :: Set String
seqMarkers = Set String
forall a. Set a
Set.empty
  }

unionTI :: TextInfo -> TextInfo -> TextInfo
unionTI :: TextInfo -> TextInfo -> TextInfo
unionTI s :: TextInfo
s t :: TextInfo
t = TextInfo :: MapSet String Int
-> MapSet String Int
-> MapSet String Int
-> MapSet String Int
-> Set String
-> TextInfo
TextInfo
  { arityPred :: MapSet String Int
arityPred = (MapSet String Int -> MapSet String Int -> MapSet String Int)
-> (TextInfo -> MapSet String Int)
-> TextInfo
-> TextInfo
-> MapSet String Int
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on MapSet String Int -> MapSet String Int -> MapSet String Int
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.union TextInfo -> MapSet String Int
arityPred TextInfo
s TextInfo
t
  , arityFunc :: MapSet String Int
arityFunc = (MapSet String Int -> MapSet String Int -> MapSet String Int)
-> (TextInfo -> MapSet String Int)
-> TextInfo
-> TextInfo
-> MapSet String Int
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on MapSet String Int -> MapSet String Int -> MapSet String Int
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.union TextInfo -> MapSet String Int
arityFunc TextInfo
s TextInfo
t
  , boundPred :: MapSet String Int
boundPred = (MapSet String Int -> MapSet String Int -> MapSet String Int)
-> (TextInfo -> MapSet String Int)
-> TextInfo
-> TextInfo
-> MapSet String Int
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on MapSet String Int -> MapSet String Int -> MapSet String Int
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.union TextInfo -> MapSet String Int
boundPred TextInfo
s TextInfo
t
  , boundFunc :: MapSet String Int
boundFunc = (MapSet String Int -> MapSet String Int -> MapSet String Int)
-> (TextInfo -> MapSet String Int)
-> TextInfo
-> TextInfo
-> MapSet String Int
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on MapSet String Int -> MapSet String Int -> MapSet String Int
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.union TextInfo -> MapSet String Int
boundFunc TextInfo
s TextInfo
t
  , seqMarkers :: Set String
seqMarkers = (Set String -> Set String -> Set String)
-> (TextInfo -> Set String) -> TextInfo -> TextInfo -> Set String
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on Set String -> Set String -> Set String
forall a. Ord a => Set a -> Set a -> Set a
Set.union TextInfo -> Set String
seqMarkers TextInfo
s TextInfo
t
  }

unionsTI :: [TextInfo] -> TextInfo
unionsTI :: [TextInfo] -> TextInfo
unionsTI = (TextInfo -> TextInfo -> TextInfo)
-> TextInfo -> [TextInfo] -> TextInfo
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TextInfo -> TextInfo -> TextInfo
unionTI TextInfo
emptyTI

removeFromTI :: String -> TextInfo -> TextInfo
removeFromTI :: String -> TextInfo -> TextInfo
removeFromTI n :: String
n ti :: TextInfo
ti = let deln :: MapSet String b -> MapSet String b
deln = Map String (Set b) -> MapSet String b
forall a b. Ord a => Map a (Set b) -> MapSet a b
MapSet.fromMap (Map String (Set b) -> MapSet String b)
-> (MapSet String b -> Map String (Set b))
-> MapSet String b
-> MapSet String b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Map String (Set b) -> Map String (Set b)
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete String
n (Map String (Set b) -> Map String (Set b))
-> (MapSet String b -> Map String (Set b))
-> MapSet String b
-> Map String (Set b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSet String b -> Map String (Set b)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap in
  TextInfo
ti
  { arityPred :: MapSet String Int
arityPred = MapSet String Int -> MapSet String Int
forall b. MapSet String b -> MapSet String b
deln (MapSet String Int -> MapSet String Int)
-> MapSet String Int -> MapSet String Int
forall a b. (a -> b) -> a -> b
$ TextInfo -> MapSet String Int
arityPred TextInfo
ti
  , arityFunc :: MapSet String Int
arityFunc = MapSet String Int -> MapSet String Int
forall b. MapSet String b -> MapSet String b
deln (MapSet String Int -> MapSet String Int)
-> MapSet String Int -> MapSet String Int
forall a b. (a -> b) -> a -> b
$ TextInfo -> MapSet String Int
arityFunc TextInfo
ti
  , seqMarkers :: Set String
seqMarkers = String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.delete String
n (Set String -> Set String) -> Set String -> Set String
forall a b. (a -> b) -> a -> b
$ TextInfo -> Set String
seqMarkers TextInfo
ti
  }

mapSub :: ClSl.CommonLogicSL -> CSL.CASL_Sublogics
mapSub :: CommonLogicSL -> CASL_Sublogics
mapSub _ = CASL_Sublogics
forall a. Lattice a => CASL_SL a
CSL.cFol
        { cons_features :: SortGenerationFeatures
CSL.cons_features = SortGenerationFeatures
CSL.emptyMapConsFeature }

-- unsuitable, mere signatures cannot be mapped properly!
mapMor :: CommonLogicSL -> ClMor.Morphism -> Result CMor.CASLMor
mapMor :: CommonLogicSL -> Morphism -> Result CASLMor
mapMor b :: CommonLogicSL
b mor :: Morphism
mor = CASLMor -> Result CASLMor
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> CASLSign -> CASLSign -> CASLMor
forall m f e. m -> Sign f e -> Sign f e -> Morphism f e m
CMor.embedMorphism ()
  (CommonLogicSL -> TextInfo -> CASLSign
mapSig CommonLogicSL
b TextInfo
emptyTI) (CASLSign -> CASLMor) -> CASLSign -> CASLMor
forall a b. (a -> b) -> a -> b
$ CommonLogicSL -> TextInfo -> CASLSign
mapSig CommonLogicSL
b TextInfo
emptyTI)
  { pred_map :: Pred_map
CMor.pred_map = Map Id Id -> Pred_map
trMor (Map Id Id -> Pred_map) -> Map Id Id -> Pred_map
forall a b. (a -> b) -> a -> b
$ Morphism -> Map Id Id
ClMor.propMap Morphism
mor }

-- | Helper for map mor
trMor :: Map.Map Id Id -> Map.Map (Id, PredType) Id
trMor :: Map Id Id -> Pred_map
trMor mp :: Map Id Id
mp =
    let
        pt :: PredType
pt = PredType :: [Id] -> PredType
PredType {predArgs :: [Id]
predArgs = []}
        id2Id :: Id -> Id
id2Id = Token -> Id
tok2Id (Token -> Id) -> (Id -> Token) -> Id -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Token
mkSimpleId (String -> Token) -> (Id -> String) -> Id -> Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> String
forall a. Show a => a -> String
show
    in
      (Id -> Id -> Pred_map -> Pred_map)
-> Pred_map -> Map Id Id -> Pred_map
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey
             (\ k :: Id
k a :: Id
a ->
              (Id, PredType) -> Id -> Pred_map -> Pred_map
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id -> Id
id2Id Id
k, PredType
pt) (Id -> Pred_map -> Pred_map) -> Id -> Pred_map -> Pred_map
forall a b. (a -> b) -> a -> b
$ Id -> Id
id2Id Id
a
             )
      Pred_map
forall k a. Map k a
Map.empty
      Map Id Id
mp

mapTheory :: CommonLogicSL -> (ClSign.Sign, [AS_Anno.Named Cl.TEXT_META])
              -> Result (CASLSign, [AS_Anno.Named CBasic.CASLFORMULA])
mapTheory :: CommonLogicSL
-> (Sign, [Named TEXT_META])
-> Result (CASLSign, [Named CASLFORMULA])
mapTheory b :: CommonLogicSL
b (_, form :: [Named TEXT_META]
form) = do
  TextInfo
ti <- ([TextInfo] -> TextInfo) -> Result [TextInfo] -> Result TextInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [TextInfo] -> TextInfo
unionsTI (Result [TextInfo] -> Result TextInfo)
-> Result [TextInfo] -> Result TextInfo
forall a b. (a -> b) -> a -> b
$ (Named TEXT_META -> Result TextInfo)
-> [Named TEXT_META] -> Result [TextInfo]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TEXT_META -> Result TextInfo
collectTextInfo (TEXT_META -> Result TextInfo)
-> (Named TEXT_META -> TEXT_META)
-> Named TEXT_META
-> Result TextInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named TEXT_META -> TEXT_META
forall s a. SenAttr s a -> s
AS_Anno.sentence) [Named TEXT_META]
form
  [Named CASLFORMULA]
frm <- (Named TEXT_META -> Result (Named CASLFORMULA))
-> [Named TEXT_META] -> Result [Named CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CommonLogicSL -> Named TEXT_META -> Result (Named CASLFORMULA)
trNamedForm CommonLogicSL
b) [Named TEXT_META]
form
  let s :: CASLSign
s = CommonLogicSL -> TextInfo -> CASLSign
mapSig CommonLogicSL
b TextInfo
ti
  (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return ((CASLSign, [Named CASLFORMULA])
 -> Result (CASLSign, [Named CASLFORMULA]))
-> (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall a b. (a -> b) -> a -> b
$ if CommonLogicSL -> Bool
compact CommonLogicSL
b then (CASLSign
s, [Named CASLFORMULA]
frm) else
    (CASLSign -> CASLSign -> CASLSign
uniteCASLSign CASLSign
listSig CASLSign
s, [Named CASLFORMULA]
baseListAxioms [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
frm)

funS :: String
funS :: String
funS = "fun"

relS :: String
relS :: String
relS = "rel"

seqType :: OpType
seqType :: OpType
seqType = [Id] -> Id -> OpType
mkTotOpType [Id
list] Id
individual

seqFunType :: OpType
seqFunType :: OpType
seqFunType = [Id] -> Id -> OpType
mkTotOpType [Id
individual, Id
list] Id
individual

seqRelType :: PredType
seqRelType :: PredType
seqRelType = [Id] -> PredType
PredType [Id
individual, Id
list]

mapNs :: Ord a => MapSet String a -> MapSet Id a
mapNs :: MapSet String a -> MapSet Id a
mapNs = (String -> a -> MapSet Id a -> MapSet Id a)
-> MapSet Id a -> MapSet String a -> MapSet Id a
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey (Id -> a -> MapSet Id a -> MapSet Id a
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert (Id -> a -> MapSet Id a -> MapSet Id a)
-> (String -> Id) -> String -> a -> MapSet Id a -> MapSet Id a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Id
stringToId) MapSet Id a
forall a b. MapSet a b
MapSet.empty

mapSig :: CommonLogicSL -> TextInfo -> CASLSign
mapSig :: CommonLogicSL -> TextInfo -> CASLSign
mapSig b :: CommonLogicSL
b ti :: TextInfo
ti =
  let isFol :: Bool
isFol = CommonLogicSL -> CLTextType
format CommonLogicSL
b CLTextType -> CLTextType -> Bool
forall a. Ord a => a -> a -> Bool
<= CLTextType
FirstOrder
      isC :: Bool
isC = CommonLogicSL -> Bool
compact CommonLogicSL
b
      aF :: MapSet String Int
aF = TextInfo -> MapSet String Int
arityFunc TextInfo
ti
      (aC :: MapSet String Int
aC, aRF :: MapSet String Int
aRF) = (Int -> Bool)
-> MapSet String Int -> (MapSet String Int, MapSet String Int)
forall a b.
(Ord a, Ord b) =>
(b -> Bool) -> MapSet a b -> (MapSet a b, MapSet a b)
MapSet.partition (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0) MapSet String Int
aF
      aA :: MapSet String Int
aA = MapSet String Int -> MapSet String Int -> MapSet String Int
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.union MapSet String Int
aF MapSet String Int
aP
      collM :: a -> MapSet a b -> MapSet a b
collM n :: a
n = Map a (Set b) -> MapSet a b
forall a b. Ord a => Map a (Set b) -> MapSet a b
MapSet.fromMap (Map a (Set b) -> MapSet a b)
-> (MapSet a b -> Map a (Set b)) -> MapSet a b -> MapSet a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Set b -> Map a (Set b)
forall k a. k -> a -> Map k a
Map.singleton a
n (Set b -> Map a (Set b))
-> (MapSet a b -> Set b) -> MapSet a b -> Map a (Set b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> b) -> Set b -> Set b
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (b -> b -> b
forall a. Num a => a -> a -> a
+ 1) (Set b -> Set b) -> (MapSet a b -> Set b) -> MapSet a b -> Set b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSet a b -> Set b
forall b a. Ord b => MapSet a b -> Set b
MapSet.elems
      om :: MapSet Id OpType
om = if Bool
isC then
        (String -> Int -> MapSet Id OpType -> MapSet Id OpType)
-> MapSet Id OpType -> MapSet String Int -> MapSet Id OpType
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey (\ n :: String
n ar :: Int
ar ops :: MapSet Id OpType
ops ->
          Id -> OpType -> MapSet Id OpType -> MapSet Id OpType
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert (String -> Id
stringToId String
n) (Int -> OpType
opTypeSign Int
ar) MapSet Id OpType
ops
        ) MapSet Id OpType
forall a b. MapSet a b
MapSet.empty
          (MapSet String Int -> MapSet Id OpType)
-> MapSet String Int -> MapSet Id OpType
forall a b. (a -> b) -> a -> b
$ if Bool
isFol then MapSet String Int
aF else
              MapSet String Int -> MapSet String Int -> MapSet String Int
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.union ((Set Int -> Set Int) -> MapSet String Int -> MapSet String Int
forall a b c. Ord a => (Set b -> Set c) -> MapSet a b -> MapSet a c
MapSet.mapSet (Set Int -> Set Int -> Set Int
forall a b. a -> b -> a
const (Set Int -> Set Int -> Set Int) -> Set Int -> Set Int -> Set Int
forall a b. (a -> b) -> a -> b
$ Int -> Set Int
forall a. a -> Set a
Set.singleton 0) MapSet String Int
aA)
              (MapSet String Int -> MapSet String Int)
-> MapSet String Int -> MapSet String Int
forall a b. (a -> b) -> a -> b
$ String -> MapSet String Int -> MapSet String Int
forall a b a.
(Ord a, Ord b, Num b) =>
a -> MapSet a b -> MapSet a b
collM String
funS (MapSet String Int -> MapSet String Int)
-> MapSet String Int -> MapSet String Int
forall a b. (a -> b) -> a -> b
$ (Set Int -> Set Int) -> MapSet String Int -> MapSet String Int
forall a b c. Ord a => (Set b -> Set c) -> MapSet a b -> MapSet a c
MapSet.mapSet (Int -> Set Int -> Set Int
forall a. Ord a => a -> Set a -> Set a
Set.delete 0) (MapSet String Int -> MapSet String Int)
-> MapSet String Int -> MapSet String Int
forall a b. (a -> b) -> a -> b
$ TextInfo -> MapSet String Int
boundFunc TextInfo
ti
        else MapSet String OpType -> MapSet Id OpType
forall a. Ord a => MapSet String a -> MapSet Id a
mapNs
             (MapSet String OpType -> MapSet Id OpType)
-> MapSet String OpType -> MapSet Id OpType
forall a b. (a -> b) -> a -> b
$ MapSet String OpType
-> MapSet String OpType -> MapSet String OpType
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.union
               (if Bool
isFol then
                 (Set Int -> Set OpType)
-> MapSet String Int -> MapSet String OpType
forall a b c. Ord a => (Set b -> Set c) -> MapSet a b -> MapSet a c
MapSet.mapSet (Set OpType -> Set Int -> Set OpType
forall a b. a -> b -> a
const (Set OpType -> Set Int -> Set OpType)
-> Set OpType -> Set Int -> Set OpType
forall a b. (a -> b) -> a -> b
$ OpType -> Set OpType
forall a. a -> Set a
Set.singleton OpType
seqType) MapSet String Int
aRF
               else String -> OpType -> MapSet String OpType -> MapSet String OpType
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert String
funS OpType
seqFunType MapSet String OpType
forall a b. MapSet a b
MapSet.empty)
             (MapSet String OpType -> MapSet String OpType)
-> MapSet String OpType -> MapSet String OpType
forall a b. (a -> b) -> a -> b
$ MapSet String OpType
-> MapSet String OpType -> MapSet String OpType
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.union ((Set Int -> Set OpType)
-> MapSet String Int -> MapSet String OpType
forall a b c. Ord a => (Set b -> Set c) -> MapSet a b -> MapSet a c
MapSet.mapSet (Set OpType -> Set Int -> Set OpType
forall a b. a -> b -> a
const (Set OpType -> Set Int -> Set OpType)
-> Set OpType -> Set Int -> Set OpType
forall a b. (a -> b) -> a -> b
$ OpType -> Set OpType
forall a. a -> Set a
Set.singleton
               (OpType -> Set OpType) -> OpType -> Set OpType
forall a b. (a -> b) -> a -> b
$ [Id] -> Id -> OpType
mkTotOpType [] Id
individual) (MapSet String Int -> MapSet String OpType)
-> MapSet String Int -> MapSet String OpType
forall a b. (a -> b) -> a -> b
$ if Bool
isFol then MapSet String Int
aC else MapSet String Int
aA)
             (MapSet String OpType -> MapSet String OpType)
-> MapSet String OpType -> MapSet String OpType
forall a b. (a -> b) -> a -> b
$ [(String, [OpType])] -> MapSet String OpType
forall a b. (Ord a, Ord b) => [(a, [b])] -> MapSet a b
MapSet.fromList
             ([(String, [OpType])] -> MapSet String OpType)
-> [(String, [OpType])] -> MapSet String OpType
forall a b. (a -> b) -> a -> b
$ (String -> (String, [OpType])) -> [String] -> [(String, [OpType])]
forall a b. (a -> b) -> [a] -> [b]
map (\ s :: String
s -> (String
s, [[Id] -> Id -> OpType
mkTotOpType [] Id
list]))
             ([String] -> [(String, [OpType])])
-> [String] -> [(String, [OpType])]
forall a b. (a -> b) -> a -> b
$ Set String -> [String]
forall a. Set a -> [a]
Set.toList (Set String -> [String]) -> Set String -> [String]
forall a b. (a -> b) -> a -> b
$ TextInfo -> Set String
seqMarkers TextInfo
ti
      aP :: MapSet String Int
aP = TextInfo -> MapSet String Int
arityPred TextInfo
ti
      pm :: MapSet Id PredType
pm | Bool
isC =
            (String -> Int -> MapSet Id PredType -> MapSet Id PredType)
-> MapSet Id PredType -> MapSet String Int -> MapSet Id PredType
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey (\ n :: String
n ar :: Int
ar preds :: MapSet Id PredType
preds ->
            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 (String -> Id
stringToId String
n) (Int -> PredType
predTypeSign Int
ar) MapSet Id PredType
preds
            ) MapSet Id PredType
forall a b. MapSet a b
MapSet.empty (MapSet String Int -> MapSet Id PredType)
-> MapSet String Int -> MapSet Id PredType
forall a b. (a -> b) -> a -> b
$ if Bool
isFol then MapSet String Int
aP else String -> MapSet String Int -> MapSet String Int
forall a b a.
(Ord a, Ord b, Num b) =>
a -> MapSet a b -> MapSet a b
collM String
relS (MapSet String Int -> MapSet String Int)
-> MapSet String Int -> MapSet String Int
forall a b. (a -> b) -> a -> b
$ TextInfo -> MapSet String Int
boundPred TextInfo
ti
         | Bool
isFol = MapSet String PredType -> MapSet Id PredType
forall a. Ord a => MapSet String a -> MapSet Id a
mapNs (MapSet String PredType -> MapSet Id PredType)
-> MapSet String PredType -> MapSet Id PredType
forall a b. (a -> b) -> a -> b
$ (Set Int -> Set PredType)
-> MapSet String Int -> MapSet String PredType
forall a b c. Ord a => (Set b -> Set c) -> MapSet a b -> MapSet a c
MapSet.mapSet (Set PredType -> Set Int -> Set PredType
forall a b. a -> b -> a
const (Set PredType -> Set Int -> Set PredType)
-> Set PredType -> Set Int -> Set PredType
forall a b. (a -> b) -> a -> b
$ PredType -> Set PredType
forall a. a -> Set a
Set.singleton
            (PredType -> Set PredType) -> PredType -> Set PredType
forall a b. (a -> b) -> a -> b
$ [Id] -> PredType
PredType [Id
list]) MapSet String Int
aP
         | Bool
otherwise = 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 (String -> Id
stringToId String
relS) PredType
seqRelType MapSet Id PredType
forall a b. MapSet a b
MapSet.empty
  in (() -> CASLSign
forall e f. e -> Sign f e
emptySign ())
            { sortRel :: Rel Id
sortRel = Id -> Rel Id -> Rel Id
forall a. Ord a => a -> Rel a -> Rel a
Rel.insertKey Id
individual Rel Id
forall a. Rel a
Rel.empty
            , opMap :: MapSet Id OpType
opMap = MapSet Id OpType
om
            , predMap :: MapSet Id PredType
predMap = MapSet Id PredType
pm
            }

opTypeSign :: Int -> OpType
opTypeSign :: Int -> OpType
opTypeSign ar :: Int
ar = [Id] -> Id -> OpType
mkTotOpType (Int -> Id -> [Id]
forall a. Int -> a -> [a]
replicate Int
ar Id
individual) Id
individual

predTypeSign :: Int -> PredType
predTypeSign :: Int -> PredType
predTypeSign ar :: Int
ar = PredType :: [Id] -> PredType
PredType {predArgs :: [Id]
predArgs = Int -> Id -> [Id]
forall a. Int -> a -> [a]
replicate Int
ar Id
individual}

trNamedForm :: CommonLogicSL -> AS_Anno.Named Cl.TEXT_META
            -> Result (AS_Anno.Named CBasic.CASLFORMULA)
trNamedForm :: CommonLogicSL -> Named TEXT_META -> Result (Named CASLFORMULA)
trNamedForm b :: CommonLogicSL
b = (TEXT_META -> Result CASLFORMULA)
-> Named TEXT_META -> Result (Named CASLFORMULA)
forall (m :: * -> *) s t.
Monad m =>
(s -> m t) -> Named s -> m (Named t)
AS_Anno.mapNamedM ((TEXT_META -> Result CASLFORMULA)
 -> Named TEXT_META -> Result (Named CASLFORMULA))
-> (TEXT_META -> Result CASLFORMULA)
-> Named TEXT_META
-> Result (Named CASLFORMULA)
forall a b. (a -> b) -> a -> b
$ CommonLogicSL -> TEXT_META -> Result CASLFORMULA
trFormMeta CommonLogicSL
b (TEXT_META -> Result CASLFORMULA)
-> (TEXT_META -> TEXT_META) -> TEXT_META -> Result CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TEXT_META -> TEXT_META
eliminateModules

mapSentence :: CommonLogicSL -> Cl.TEXT_META -> Result CBasic.CASLFORMULA
mapSentence :: CommonLogicSL -> TEXT_META -> Result CASLFORMULA
mapSentence b :: CommonLogicSL
b = CommonLogicSL -> TEXT_META -> Result CASLFORMULA
trFormMeta CommonLogicSL
b (TEXT_META -> Result CASLFORMULA)
-> (TEXT_META -> TEXT_META) -> TEXT_META -> Result CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TEXT_META -> TEXT_META
eliminateModules

-- ignores importations
trFormMeta :: CommonLogicSL -> Cl.TEXT_META -> Result CBasic.CASLFORMULA
trFormMeta :: CommonLogicSL -> TEXT_META -> Result CASLFORMULA
trFormMeta b :: CommonLogicSL
b tm :: TEXT_META
tm = CommonLogicSL -> TEXT -> Result CASLFORMULA
trForm CommonLogicSL
b (TEXT -> Result CASLFORMULA) -> TEXT -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ TEXT_META -> TEXT
Cl.getText TEXT_META
tm

trForm :: CommonLogicSL -> Cl.TEXT -> Result CBasic.CASLFORMULA
trForm :: CommonLogicSL -> TEXT -> Result CASLFORMULA
trForm b :: CommonLogicSL
b form :: TEXT
form =
   case TEXT
form of
     Cl.Text phrs :: [PHRASE]
phrs rn :: Range
rn -> do
        [CASLFORMULA]
phrsfrm <- (PHRASE -> Result CASLFORMULA) -> [PHRASE] -> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CommonLogicSL -> PHRASE -> Result CASLFORMULA
phraseForm CommonLogicSL
b) ([PHRASE] -> Result [CASLFORMULA])
-> [PHRASE] -> Result [CASLFORMULA]
forall a b. (a -> b) -> a -> b
$ (PHRASE -> Bool) -> [PHRASE] -> [PHRASE]
forall a. (a -> Bool) -> [a] -> [a]
filter PHRASE -> Bool
nonImportAndNonEmpty [PHRASE]
phrs
        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] -> Range -> CASLFORMULA
forall f. [FORMULA f] -> Range -> FORMULA f
CBasic.conjunctRange [CASLFORMULA]
phrsfrm Range
rn
     Cl.Named_text _ t :: TEXT
t _ -> CommonLogicSL -> TEXT -> Result CASLFORMULA
trForm CommonLogicSL
b TEXT
t
   where nonImportAndNonEmpty :: Cl.PHRASE -> Bool
         nonImportAndNonEmpty :: PHRASE -> Bool
nonImportAndNonEmpty p :: PHRASE
p = case PHRASE
p of
            Cl.Importation _ -> Bool
False
            Cl.Comment_text _ t :: TEXT
t _ -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ TEXT -> Bool
isTextEmpty TEXT
t
            _ -> Bool
True
         isTextEmpty :: Cl.TEXT -> Bool
         isTextEmpty :: TEXT -> Bool
isTextEmpty txt :: TEXT
txt = case TEXT
txt of
            Cl.Named_text _ t :: TEXT
t _ -> TEXT -> Bool
isTextEmpty TEXT
t
            Cl.Text [] _ -> Bool
True
            _ -> Bool
False

phraseForm :: CommonLogicSL -> Cl.PHRASE -> Result CBasic.CASLFORMULA
phraseForm :: CommonLogicSL -> PHRASE -> Result CASLFORMULA
phraseForm b :: CommonLogicSL
b phr :: PHRASE
phr = case PHRASE
phr of
  Cl.Module _ -> String -> Result CASLFORMULA
forall a. HasCallStack => String -> a
error "CL2CFOL.phraseForm.Module"
  -- cannot occur because module elimination applied
  Cl.Sentence s :: SENTENCE
s -> CommonLogicSL -> Set Token -> SENTENCE -> Result CASLFORMULA
senForm CommonLogicSL
b Set Token
forall a. Set a
Set.empty SENTENCE
s
  Cl.Importation _ -> String -> Result CASLFORMULA
forall a. HasCallStack => String -> a
error "CL2CFOL.phraseForm.Importation"
  -- cannot occur, because filtered
  Cl.Comment_text _ t :: TEXT
t _ -> CommonLogicSL -> TEXT -> Result CASLFORMULA
trForm CommonLogicSL
b TEXT
t

senForm :: CommonLogicSL -> Set.Set Cl.NAME -> Cl.SENTENCE
  -> Result CBasic.CASLFORMULA
senForm :: CommonLogicSL -> Set Token -> SENTENCE -> Result CASLFORMULA
senForm b :: CommonLogicSL
b bndVars :: Set Token
bndVars form :: SENTENCE
form = case SENTENCE
form of
  Cl.Bool_sent bs :: BOOL_SENT
bs rn :: Range
rn -> case BOOL_SENT
bs of
      Cl.Negation s :: SENTENCE
s -> do
          CASLFORMULA
sen <- CommonLogicSL -> Set Token -> SENTENCE -> Result CASLFORMULA
senForm CommonLogicSL
b Set Token
bndVars SENTENCE
s
          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 -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
CBasic.Negation CASLFORMULA
sen Range
rn
      Cl.Junction j :: AndOr
j ss :: [SENTENCE]
ss -> do
          [CASLFORMULA]
sens <- (SENTENCE -> Result CASLFORMULA)
-> [SENTENCE] -> Result [CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CommonLogicSL -> Set Token -> SENTENCE -> Result CASLFORMULA
senForm CommonLogicSL
b Set Token
bndVars) [SENTENCE]
ss
          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
$ (case AndOr
j of
            Cl.Conjunction -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. [FORMULA f] -> Range -> FORMULA f
CBasic.conjunctRange
            Cl.Disjunction -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. [FORMULA f] -> Range -> FORMULA f
CBasic.disjunctRange) [CASLFORMULA]
sens Range
rn
      Cl.BinOp j :: ImplEq
j s1 :: SENTENCE
s1 s2 :: SENTENCE
s2 -> do
          CASLFORMULA
sen1 <- CommonLogicSL -> Set Token -> SENTENCE -> Result CASLFORMULA
senForm CommonLogicSL
b Set Token
bndVars SENTENCE
s1
          CASLFORMULA
sen2 <- CommonLogicSL -> Set Token -> SENTENCE -> Result CASLFORMULA
senForm CommonLogicSL
b Set Token
bndVars SENTENCE
s2
          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 -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
CBasic.Relation CASLFORMULA
sen1 (case ImplEq
j of
            Cl.Implication -> Relation
CBasic.Implication
            Cl.Biconditional -> Relation
CBasic.Equivalence) CASLFORMULA
sen2 Range
rn
  Cl.Quant_sent q :: QUANT
q bs :: [NAME_OR_SEQMARK]
bs s :: SENTENCE
s rn :: Range
rn ->
        CommonLogicSL
-> QUANTIFIER
-> Range
-> Set Token
-> [NAME_OR_SEQMARK]
-> SENTENCE
-> Result CASLFORMULA
quantSentForm CommonLogicSL
b (case QUANT
q of
          Cl.Universal -> QUANTIFIER
CBasic.Universal
          Cl.Existential -> QUANTIFIER
CBasic.Existential) Range
rn Set Token
bndVars [NAME_OR_SEQMARK]
bs SENTENCE
s
  Cl.Atom_sent at :: ATOM
at rn :: Range
rn -> case ATOM
at of
      Cl.Equation trm1 :: TERM
trm1 trm2 :: TERM
trm2 -> do
          TERM ()
t1 <- CommonLogicSL -> Set Token -> TERM -> Result (TERM ())
termForm CommonLogicSL
b Set Token
bndVars TERM
trm1
          TERM ()
t2 <- CommonLogicSL -> Set Token -> TERM -> Result (TERM ())
termForm CommonLogicSL
b Set Token
bndVars TERM
trm2
          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
$ TERM () -> Equality -> TERM () -> Range -> CASLFORMULA
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
CBasic.Equation TERM ()
t1 Equality
CBasic.Strong TERM ()
t2 Range
rn
      Cl.Atom trm :: TERM
trm tseqs :: [TERM_SEQ]
tseqs -> do
          let (rt :: TERM
rt, rseq :: [TERM_SEQ]
rseq) = TERM -> [TERM_SEQ] -> (TERM, [TERM_SEQ])
uncurryTermWithArgs TERM
trm [TERM_SEQ]
tseqs
          [TERM ()]
trmSeqs <- CommonLogicSL -> Set Token -> [TERM_SEQ] -> Result [TERM ()]
termSeq CommonLogicSL
b Set Token
bndVars [TERM_SEQ]
rseq
          let ar :: Int
ar = [TERM_SEQ] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TERM_SEQ]
rseq
              isC :: Bool
isC = CommonLogicSL -> Bool
compact CommonLogicSL
b
          if CommonLogicSL -> CLTextType
format CommonLogicSL
b CLTextType -> CLTextType -> Bool
forall a. Ord a => a -> a -> Bool
<= CLTextType
FirstOrder then do
              PRED_SYMB
trmFP <- TERM -> Maybe Int -> Result PRED_SYMB
termFormPrd TERM
rt
                (Maybe Int -> Result PRED_SYMB) -> Maybe Int -> Result PRED_SYMB
forall a b. (a -> b) -> a -> b
$ if Bool
isC then Int -> Maybe Int
forall a. a -> Maybe a
Just Int
ar else Maybe Int
forall a. Maybe a
Nothing
              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
$ PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
CBasic.Predication PRED_SYMB
trmFP [TERM ()]
trmSeqs Range
rn
            else do
              TERM ()
trm1 <- CommonLogicSL -> Set Token -> TERM -> Result (TERM ())
termForm CommonLogicSL
b Set Token
bndVars TERM
rt
              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
$ PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
CBasic.Predication
                (Id -> PRED_TYPE -> PRED_SYMB
CBasic.mkQualPred (String -> Id
stringToId String
relS)
                (PRED_TYPE -> PRED_SYMB) -> PRED_TYPE -> PRED_SYMB
forall a b. (a -> b) -> a -> b
$ if Bool
isC then Int -> PRED_TYPE
predType (Int -> PRED_TYPE) -> Int -> PRED_TYPE
forall a b. (a -> b) -> a -> b
$ Int
ar Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 else PredType -> PRED_TYPE
toPRED_TYPE PredType
seqRelType)
                (TERM ()
trm1 TERM () -> [TERM ()] -> [TERM ()]
forall a. a -> [a] -> [a]
: [TERM ()]
trmSeqs) Range
rn
  Cl.Comment_sent _ s :: SENTENCE
s _ -> CommonLogicSL -> Set Token -> SENTENCE -> Result CASLFORMULA
senForm CommonLogicSL
b Set Token
bndVars SENTENCE
s
  Cl.Irregular_sent s :: SENTENCE
s _ -> CommonLogicSL -> Set Token -> SENTENCE -> Result CASLFORMULA
senForm CommonLogicSL
b Set Token
bndVars SENTENCE
s

-- checks for second order quantification
quantSentForm :: CommonLogicSL -> QUANTIFIER -> Range -> Set.Set Cl.NAME
  -> [Cl.NAME_OR_SEQMARK] -> Cl.SENTENCE -> Result CBasic.CASLFORMULA
quantSentForm :: CommonLogicSL
-> QUANTIFIER
-> Range
-> Set Token
-> [NAME_OR_SEQMARK]
-> SENTENCE
-> Result CASLFORMULA
quantSentForm b :: CommonLogicSL
b quantifier :: QUANTIFIER
quantifier rn :: Range
rn bndVars :: Set Token
bndVars bs :: [NAME_OR_SEQMARK]
bs sen :: SENTENCE
sen = do
  CASLFORMULA
folSen <- if [NAME_OR_SEQMARK] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NAME_OR_SEQMARK]
bs
            then CommonLogicSL -> Set Token -> SENTENCE -> Result CASLFORMULA
senForm CommonLogicSL
b Set Token
bndVars SENTENCE
sen
            else do
              Set Token
bndVarsSet <- Set Token -> [NAME_OR_SEQMARK] -> Result (Set Token)
bndVarsToSet Set Token
bndVars [NAME_OR_SEQMARK]
bs
              CASLFORMULA
sf <- CommonLogicSL -> Set Token -> SENTENCE -> Result CASLFORMULA
senForm CommonLogicSL
b Set Token
bndVarsSet SENTENCE
sen
              [VAR_DECL]
bindSeq <- (NAME_OR_SEQMARK -> Result VAR_DECL)
-> [NAME_OR_SEQMARK] -> Result [VAR_DECL]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM NAME_OR_SEQMARK -> Result VAR_DECL
bindingSeq [NAME_OR_SEQMARK]
bs
              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
$ QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
CBasic.Quantification QUANTIFIER
quantifier [VAR_DECL]
bindSeq CASLFORMULA
sf Range
rn
  CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return CASLFORMULA
folSen

opType :: Int -> CBasic.OP_TYPE
opType :: Int -> OP_TYPE
opType ar :: Int
ar =
  OpKind -> [Id] -> Id -> Range -> OP_TYPE
CBasic.Op_type OpKind
CBasic.Total (Int -> Id -> [Id]
forall a. Int -> a -> [a]
replicate Int
ar Id
individual) Id
individual Range
nullRange

predType :: Int -> CBasic.PRED_TYPE
predType :: Int -> PRED_TYPE
predType ar :: Int
ar = [Id] -> Range -> PRED_TYPE
CBasic.Pred_type (Int -> Id -> [Id]
forall a. Int -> a -> [a]
replicate Int
ar Id
individual) Range
nullRange

bndVarsToSet :: Set.Set Cl.NAME -> [Cl.NAME_OR_SEQMARK]
  -> Result (Set.Set Cl.NAME)
bndVarsToSet :: Set Token -> [NAME_OR_SEQMARK] -> Result (Set Token)
bndVarsToSet bndVars :: Set Token
bndVars bs :: [NAME_OR_SEQMARK]
bs = do
  [Token]
res <- (NAME_OR_SEQMARK -> Result Token)
-> [NAME_OR_SEQMARK] -> Result [Token]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ nos :: NAME_OR_SEQMARK
nos -> Token -> Result Token
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> Result Token) -> Token -> Result Token
forall a b. (a -> b) -> a -> b
$ case NAME_OR_SEQMARK
nos of
                  Cl.Name n :: Token
n -> Token
n
                  Cl.SeqMark s :: Token
s -> Token
s)
        [NAME_OR_SEQMARK]
bs
  Set Token -> Result (Set Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set Token -> Result (Set Token))
-> Set Token -> Result (Set Token)
forall a b. (a -> b) -> a -> b
$ (Token -> Set Token -> Set Token)
-> Set Token -> [Token] -> Set Token
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Token -> Set Token -> Set Token
forall a. Ord a => a -> Set a -> Set a
Set.insert Set Token
bndVars [Token]
res

termForm :: CommonLogicSL -> Set.Set Cl.NAME -> Cl.TERM
  -> Result (CBasic.TERM ())
termForm :: CommonLogicSL -> Set Token -> TERM -> Result (TERM ())
termForm b :: CommonLogicSL
b bndVars :: Set Token
bndVars trm :: TERM
trm = case TERM
trm of
  Cl.Name_term n :: Token
n ->
      if Token -> Set Token -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Token
n Set Token
bndVars
      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
$ Token -> Id -> Range -> TERM ()
forall f. Token -> Id -> Range -> TERM f
CBasic.Qual_var (String -> Token
mkSimpleId (String -> Token) -> String -> Token
forall a b. (a -> b) -> a -> b
$ Token -> String
tok2Str Token
n)
        Id
individual Range
nullRange
      else do
        OP_SYMB
trmFA <- TERM -> Maybe Int -> Result OP_SYMB
termFormApp TERM
trm (Int -> Maybe Int
forall a. a -> Maybe a
Just 0)
        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
$ OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
CBasic.Application OP_SYMB
trmFA [] Range
nullRange
  Cl.Funct_term oterm :: TERM
oterm oseq :: [TERM_SEQ]
oseq rn :: Range
rn -> do
      let (term :: TERM
term, tseqs :: [TERM_SEQ]
tseqs) = TERM -> [TERM_SEQ] -> (TERM, [TERM_SEQ])
uncurryTermWithArgs TERM
oterm [TERM_SEQ]
oseq
      let ar :: Int
ar = [TERM_SEQ] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TERM_SEQ]
tseqs
          isC :: Bool
isC = CommonLogicSL -> Bool
compact CommonLogicSL
b
      [TERM ()]
trmSF <- CommonLogicSL -> Set Token -> [TERM_SEQ] -> Result [TERM ()]
termSeq CommonLogicSL
b Set Token
bndVars [TERM_SEQ]
tseqs
      if CommonLogicSL -> CLTextType
format CommonLogicSL
b CLTextType -> CLTextType -> Bool
forall a. Ord a => a -> a -> Bool
<= CLTextType
FirstOrder then do
         OP_SYMB
trmFA <- TERM -> Maybe Int -> Result OP_SYMB
termFormApp TERM
term (Maybe Int -> Result OP_SYMB) -> Maybe Int -> Result OP_SYMB
forall a b. (a -> b) -> a -> b
$ if Bool
isC then Int -> Maybe Int
forall a. a -> Maybe a
Just Int
ar else Maybe Int
forall a. Maybe a
Nothing
         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
$ OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
CBasic.Application OP_SYMB
trmFA [TERM ()]
trmSF Range
rn
        else do
         TERM ()
trm1 <- CommonLogicSL -> Set Token -> TERM -> Result (TERM ())
termForm CommonLogicSL
b Set Token
bndVars TERM
term
         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
$ OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
CBasic.Application
            (Id -> OP_TYPE -> OP_SYMB
CBasic.mkQualOp (String -> Id
stringToId String
funS) (OP_TYPE -> OP_SYMB) -> OP_TYPE -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ if Bool
isC then Int -> OP_TYPE
opType (Int -> OP_TYPE) -> Int -> OP_TYPE
forall a b. (a -> b) -> a -> b
$ Int
ar Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
              else OpType -> OP_TYPE
toOP_TYPE OpType
seqFunType)
            (TERM ()
trm1 TERM () -> [TERM ()] -> [TERM ()]
forall a. a -> [a] -> [a]
: [TERM ()]
trmSF) Range
rn
  Cl.Comment_term term :: TERM
term _ _ -> CommonLogicSL -> Set Token -> TERM -> Result (TERM ())
termForm CommonLogicSL
b Set Token
bndVars TERM
term
  Cl.That_term {} -> String -> Result (TERM ())
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "CL2CFOL: that-terms not supported"

termFormApp :: Cl.TERM -> Maybe Int -> Result CBasic.OP_SYMB
termFormApp :: TERM -> Maybe Int -> Result OP_SYMB
termFormApp trm :: TERM
trm ar :: Maybe Int
ar = case TERM
trm of
  Cl.Name_term n :: Token
n -> OP_SYMB -> Result OP_SYMB
forall (m :: * -> *) a. Monad m => a -> m a
return (OP_SYMB -> Result OP_SYMB) -> OP_SYMB -> Result OP_SYMB
forall a b. (a -> b) -> a -> b
$ Id -> OP_TYPE -> OP_SYMB
mkQualOp (Token -> Id
tok2Id Token
n) (OP_TYPE -> OP_SYMB) -> OP_TYPE -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ OP_TYPE -> (Int -> OP_TYPE) -> Maybe Int -> OP_TYPE
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (OpType -> OP_TYPE
toOP_TYPE OpType
seqType)
     Int -> OP_TYPE
opType Maybe Int
ar
  Cl.Comment_term t :: TERM
t _ _ -> TERM -> Maybe Int -> Result OP_SYMB
termFormApp TERM
t Maybe Int
ar
  _ -> String -> Result OP_SYMB
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "CL2CFOL.termFormApp"

termFormPrd :: Cl.TERM -> Maybe Int -> Result CBasic.PRED_SYMB
termFormPrd :: TERM -> Maybe Int -> Result PRED_SYMB
termFormPrd trm :: TERM
trm ar :: Maybe Int
ar = case TERM
trm of
  Cl.Name_term n :: Token
n -> PRED_SYMB -> Result PRED_SYMB
forall (m :: * -> *) a. Monad m => a -> m a
return (PRED_SYMB -> Result PRED_SYMB) -> PRED_SYMB -> Result PRED_SYMB
forall a b. (a -> b) -> a -> b
$ Id -> PRED_TYPE -> PRED_SYMB
mkQualPred (Token -> Id
tok2Id Token
n) (PRED_TYPE -> PRED_SYMB) -> PRED_TYPE -> PRED_SYMB
forall a b. (a -> b) -> a -> b
$ PRED_TYPE -> (Int -> PRED_TYPE) -> Maybe Int -> PRED_TYPE
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
    ([Id] -> Range -> PRED_TYPE
Pred_type [Id
list] Range
nullRange) Int -> PRED_TYPE
predType Maybe Int
ar
  Cl.Comment_term t :: TERM
t _ _ -> TERM -> Maybe Int -> Result PRED_SYMB
termFormPrd TERM
t Maybe Int
ar
  _ -> String -> Result PRED_SYMB
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "CL2CFOL.termFormPrd"

termSeqForm :: CommonLogicSL -> Set.Set Cl.NAME -> Cl.TERM_SEQ
  -> Result (CBasic.TERM ())
termSeqForm :: CommonLogicSL -> Set Token -> TERM_SEQ -> Result (TERM ())
termSeqForm b :: CommonLogicSL
b bndVars :: Set Token
bndVars tseq :: TERM_SEQ
tseq = case TERM_SEQ
tseq of
  Cl.Term_seq trm :: TERM
trm -> CommonLogicSL -> Set Token -> TERM -> Result (TERM ())
termForm CommonLogicSL
b Set Token
bndVars TERM
trm
  Cl.Seq_marks s :: Token
s -> 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 -> Id -> TERM ()
forall f. Token -> Id -> TERM f
mkVarTerm (String -> Token
mkSimpleId (String -> Token) -> String -> Token
forall a b. (a -> b) -> a -> b
$ Token -> String
tok2Str Token
s) Id
list

termSeq, mapTermSeq, foldTermSeq :: CommonLogicSL -> Set.Set Cl.NAME
  -> [Cl.TERM_SEQ] -> Result [CBasic.TERM ()]
termSeq :: CommonLogicSL -> Set Token -> [TERM_SEQ] -> Result [TERM ()]
termSeq b :: CommonLogicSL
b = if CommonLogicSL -> Bool
compact CommonLogicSL
b then CommonLogicSL -> Set Token -> [TERM_SEQ] -> Result [TERM ()]
mapTermSeq CommonLogicSL
b else CommonLogicSL -> Set Token -> [TERM_SEQ] -> Result [TERM ()]
foldTermSeq CommonLogicSL
b

mapTermSeq :: CommonLogicSL -> Set Token -> [TERM_SEQ] -> Result [TERM ()]
mapTermSeq b :: CommonLogicSL
b bndVars :: Set Token
bndVars = (TERM_SEQ -> Result (TERM ())) -> [TERM_SEQ] -> Result [TERM ()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CommonLogicSL -> Set Token -> TERM_SEQ -> Result (TERM ())
termSeqForm CommonLogicSL
b Set Token
bndVars)

foldTermSeq :: CommonLogicSL -> Set Token -> [TERM_SEQ] -> Result [TERM ()]
foldTermSeq b :: CommonLogicSL
b bndVars :: Set Token
bndVars = (TERM () -> [TERM ()]) -> Result (TERM ()) -> Result [TERM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TERM () -> [TERM ()] -> [TERM ()]
forall a. a -> [a] -> [a]
: []) (Result (TERM ()) -> Result [TERM ()])
-> ([TERM_SEQ] -> Result (TERM ()))
-> [TERM_SEQ]
-> Result [TERM ()]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TERM_SEQ -> Result (TERM ()) -> Result (TERM ()))
-> Result (TERM ()) -> [TERM_SEQ] -> Result (TERM ())
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (CommonLogicSL
-> Set Token -> TERM_SEQ -> Result (TERM ()) -> Result (TERM ())
fTermSeq CommonLogicSL
b Set Token
bndVars) (TERM () -> Result (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return TERM ()
forall f. TERM f
mkNil)

fTermSeq :: CommonLogicSL -> Set.Set Cl.NAME -> Cl.TERM_SEQ
  -> Result (CBasic.TERM ()) -> Result (CBasic.TERM ())
fTermSeq :: CommonLogicSL
-> Set Token -> TERM_SEQ -> Result (TERM ()) -> Result (TERM ())
fTermSeq b :: CommonLogicSL
b bndVars :: Set Token
bndVars tseq :: TERM_SEQ
tseq r :: Result (TERM ())
r = do
  TERM ()
l <- Result (TERM ())
r
  case TERM_SEQ
tseq of
   Cl.Term_seq trm :: TERM
trm -> do
     TERM ()
i <- CommonLogicSL -> Set Token -> TERM -> Result (TERM ())
termForm CommonLogicSL
b Set Token
bndVars TERM
trm
     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 () -> TERM ()
forall f. TERM f -> TERM f -> TERM f
mkCons TERM ()
i TERM ()
l
   Cl.Seq_marks s :: Token
s ->
     let e :: TERM f
e = Token -> Id -> TERM f
forall f. Token -> Id -> TERM f
mkVarTerm (String -> Token
mkSimpleId (String -> Token) -> String -> Token
forall a b. (a -> b) -> a -> b
$ Token -> String
tok2Str Token
s) Id
list
     in 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
$ if TERM ()
l TERM () -> TERM () -> Bool
forall a. Eq a => a -> a -> Bool
== TERM ()
forall f. TERM f
mkNil then TERM ()
forall f. TERM f
e else TERM () -> TERM () -> TERM ()
forall f. TERM f -> TERM f -> TERM f
mkAppend TERM ()
forall f. TERM f
e TERM ()
l

bindingSeq :: Cl.NAME_OR_SEQMARK -> Result CBasic.VAR_DECL
bindingSeq :: NAME_OR_SEQMARK -> Result VAR_DECL
bindingSeq bs :: NAME_OR_SEQMARK
bs = VAR_DECL -> Result VAR_DECL
forall (m :: * -> *) a. Monad m => a -> m a
return (VAR_DECL -> Result VAR_DECL) -> VAR_DECL -> Result VAR_DECL
forall a b. (a -> b) -> a -> b
$ case NAME_OR_SEQMARK
bs of
  Cl.Name n :: Token
n -> Token -> Id -> VAR_DECL
mkVarDecl (String -> Token
mkSimpleId (String -> Token) -> String -> Token
forall a b. (a -> b) -> a -> b
$ Token -> String
tok2Str Token
n) Id
individual
  Cl.SeqMark s :: Token
s -> Token -> Id -> VAR_DECL
mkVarDecl (String -> Token
mkSimpleId (String -> Token) -> String -> Token
forall a b. (a -> b) -> a -> b
$ Token -> String
tok2Str Token
s) Id
list

collectTextInfo :: Cl.TEXT_META -> Result TextInfo
collectTextInfo :: TEXT_META -> Result TextInfo
collectTextInfo tm :: TEXT_META
tm = TEXT -> Result TextInfo
colTiTxt (TEXT -> Result TextInfo) -> TEXT -> Result TextInfo
forall a b. (a -> b) -> a -> b
$ TEXT_META -> TEXT
Cl.getText TEXT_META
tm

tok2Id :: Token -> Id
tok2Id :: Token -> Id
tok2Id = String -> Id
stringToId (String -> Id) -> (Token -> String) -> Token -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> String
tok2Str

tok2Str :: Token -> String
tok2Str :: Token -> String
tok2Str t :: Token
t = let
  r :: String
r = (Char -> String) -> ShowS
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ c :: Char
c -> if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== 'x' then [Char
c, Char
c] else [Char
c])
    ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Token -> String
tokStr Token
t
  (d :: String
d, u :: String
u) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '.') String
r
  s :: String
s = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
d then String
u else 'x' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
d) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
u
  in if String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
s [String]
casl_reserved_fwords then "x_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s else String
s

colTiTxt :: Cl.TEXT -> Result TextInfo
colTiTxt :: TEXT -> Result TextInfo
colTiTxt txt :: TEXT
txt = case TEXT
txt of
  Cl.Named_text _ t :: TEXT
t _ -> TEXT -> Result TextInfo
colTiTxt TEXT
t
  Cl.Text ps :: [PHRASE]
ps _ -> do
    [TextInfo]
cti <- (PHRASE -> Result TextInfo) -> [PHRASE] -> Result [TextInfo]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM PHRASE -> Result TextInfo
colTiPhr [PHRASE]
ps
    TextInfo -> Result TextInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (TextInfo -> Result TextInfo) -> TextInfo -> Result TextInfo
forall a b. (a -> b) -> a -> b
$ [TextInfo] -> TextInfo
unionsTI [TextInfo]
cti

colTiPhr :: Cl.PHRASE -> Result TextInfo
colTiPhr :: PHRASE -> Result TextInfo
colTiPhr p :: PHRASE
p = case PHRASE
p of
  Cl.Module (Cl.Mod _ t :: TEXT
t _) -> TEXT -> Result TextInfo
colTiTxt TEXT
t
  Cl.Module (Cl.Mod_ex _ _ t :: TEXT
t _) -> TEXT -> Result TextInfo
colTiTxt TEXT
t
  Cl.Importation _ -> TextInfo -> Result TextInfo
forall (m :: * -> *) a. Monad m => a -> m a
return TextInfo
emptyTI
  Cl.Comment_text _ t :: TEXT
t _ -> TEXT -> Result TextInfo
colTiTxt TEXT
t
  Cl.Sentence s :: SENTENCE
s -> SENTENCE -> Result TextInfo
colTiSen SENTENCE
s

colTiSen :: Cl.SENTENCE -> Result TextInfo
colTiSen :: SENTENCE -> Result TextInfo
colTiSen sen :: SENTENCE
sen = case SENTENCE
sen of
  Cl.Quant_sent _ noss :: [NAME_OR_SEQMARK]
noss s :: SENTENCE
s _ -> do
          TextInfo
cti <- SENTENCE -> Result TextInfo
colTiSen SENTENCE
s
          [String]
nossR <- (NAME_OR_SEQMARK -> Result String)
-> [NAME_OR_SEQMARK] -> Result [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM NAME_OR_SEQMARK -> Result String
nosString [NAME_OR_SEQMARK]
noss
          TextInfo -> Result TextInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (TextInfo -> Result TextInfo) -> TextInfo -> Result TextInfo
forall a b. (a -> b) -> a -> b
$ (String -> TextInfo -> TextInfo)
-> TextInfo -> [String] -> TextInfo
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> TextInfo -> TextInfo
removeFromTI TextInfo
cti [String]
nossR
  Cl.Bool_sent b :: BOOL_SENT
b _ -> case BOOL_SENT
b of
      Cl.Junction _ sens :: [SENTENCE]
sens -> do
          [TextInfo]
cti <- (SENTENCE -> Result TextInfo) -> [SENTENCE] -> Result [TextInfo]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SENTENCE -> Result TextInfo
colTiSen [SENTENCE]
sens
          TextInfo -> Result TextInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (TextInfo -> Result TextInfo) -> TextInfo -> Result TextInfo
forall a b. (a -> b) -> a -> b
$ [TextInfo] -> TextInfo
unionsTI [TextInfo]
cti
      Cl.Negation s :: SENTENCE
s -> SENTENCE -> Result TextInfo
colTiSen SENTENCE
s
      Cl.BinOp _ s1 :: SENTENCE
s1 s2 :: SENTENCE
s2 -> do
          [TextInfo]
cti <- (SENTENCE -> Result TextInfo) -> [SENTENCE] -> Result [TextInfo]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SENTENCE -> Result TextInfo
colTiSen [SENTENCE
s1, SENTENCE
s2]
          TextInfo -> Result TextInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (TextInfo -> Result TextInfo) -> TextInfo -> Result TextInfo
forall a b. (a -> b) -> a -> b
$ [TextInfo] -> TextInfo
unionsTI [TextInfo]
cti
  Cl.Atom_sent a :: ATOM
a _ -> case ATOM
a of
      Cl.Equation t1 :: TERM
t1 t2 :: TERM
t2 -> do
          [TextInfo]
cti <- (TERM -> Result TextInfo) -> [TERM] -> Result [TextInfo]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TERM -> Result TextInfo
colTiTrm [TERM
t1, TERM
t2]
          TextInfo -> Result TextInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (TextInfo -> Result TextInfo) -> TextInfo -> Result TextInfo
forall a b. (a -> b) -> a -> b
$ [TextInfo] -> TextInfo
unionsTI [TextInfo]
cti
      Cl.Atom t :: TERM
t tseqs :: [TERM_SEQ]
tseqs -> let (rt :: TERM
rt, rseq :: [TERM_SEQ]
rseq) = TERM -> [TERM_SEQ] -> (TERM, [TERM_SEQ])
uncurryTermWithArgs TERM
t [TERM_SEQ]
tseqs in
          PredOrFunc -> TERM -> [TERM_SEQ] -> Result TextInfo
colTiAddArity PredOrFunc
Pred TERM
rt [TERM_SEQ]
rseq
  Cl.Comment_sent _ s :: SENTENCE
s _ -> SENTENCE -> Result TextInfo
colTiSen SENTENCE
s
  Cl.Irregular_sent s :: SENTENCE
s _ -> SENTENCE -> Result TextInfo
colTiSen SENTENCE
s

nosString :: Cl.NAME_OR_SEQMARK -> Result String
nosString :: NAME_OR_SEQMARK -> Result String
nosString nos :: NAME_OR_SEQMARK
nos = String -> Result String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Result String)
-> (Token -> String) -> Token -> Result String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> String
tok2Str (Token -> Result String) -> Token -> Result String
forall a b. (a -> b) -> a -> b
$ case NAME_OR_SEQMARK
nos of
  Cl.Name n :: Token
n -> Token
n
  Cl.SeqMark s :: Token
s -> Token
s

colTiTrm :: Cl.TERM -> Result TextInfo
colTiTrm :: TERM -> Result TextInfo
colTiTrm trm :: TERM
trm = case TERM
trm of
  Cl.Name_term n :: Token
n -> let m :: MapSet String Int
m = String -> Int -> MapSet String Int -> MapSet String Int
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert (Token -> String
tok2Str Token
n) 0 MapSet String Int
forall a b. MapSet a b
MapSet.empty in
    TextInfo -> Result TextInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (TextInfo -> Result TextInfo) -> TextInfo -> Result TextInfo
forall a b. (a -> b) -> a -> b
$ TextInfo
emptyTI
      { arityFunc :: MapSet String Int
arityFunc = MapSet String Int
m
      , boundFunc :: MapSet String Int
boundFunc = MapSet String Int
m }
  Cl.Funct_term t :: TERM
t tseqs :: [TERM_SEQ]
tseqs _ -> let (rt :: TERM
rt, rseq :: [TERM_SEQ]
rseq) = TERM -> [TERM_SEQ] -> (TERM, [TERM_SEQ])
uncurryTermWithArgs TERM
t [TERM_SEQ]
tseqs in
      PredOrFunc -> TERM -> [TERM_SEQ] -> Result TextInfo
colTiAddArity PredOrFunc
Func TERM
rt [TERM_SEQ]
rseq
  Cl.Comment_term t :: TERM
t _ _ -> TERM -> Result TextInfo
colTiTrm TERM
t
  Cl.That_term s :: SENTENCE
s _ -> SENTENCE -> Result TextInfo
colTiSen SENTENCE
s

colTiTrmSeq :: Cl.TERM_SEQ -> Result TextInfo
colTiTrmSeq :: TERM_SEQ -> Result TextInfo
colTiTrmSeq tseq :: TERM_SEQ
tseq = case TERM_SEQ
tseq of
  Cl.Term_seq trm :: TERM
trm -> TERM -> Result TextInfo
colTiTrm TERM
trm
  Cl.Seq_marks s :: Token
s -> TextInfo -> Result TextInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (TextInfo -> Result TextInfo) -> TextInfo -> Result TextInfo
forall a b. (a -> b) -> a -> b
$ TextInfo
emptyTI
    { seqMarkers :: Set String
seqMarkers = String -> Set String
forall a. a -> Set a
Set.singleton (Token -> String
tok2Str Token
s) }

colTiAddArity :: PredOrFunc -> Cl.TERM -> [Cl.TERM_SEQ] -> Result TextInfo
colTiAddArity :: PredOrFunc -> TERM -> [TERM_SEQ] -> Result TextInfo
colTiAddArity ty :: PredOrFunc
ty trm :: TERM
trm tseqs :: [TERM_SEQ]
tseqs = case TERM
trm of
  Cl.Name_term n :: Token
n -> do
    [TextInfo]
cti <- (TERM_SEQ -> Result TextInfo) -> [TERM_SEQ] -> Result [TextInfo]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TERM_SEQ -> Result TextInfo
colTiTrmSeq [TERM_SEQ]
tseqs
    let m :: MapSet String Int
m = String -> Int -> MapSet String Int -> MapSet String Int
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert (Token -> String
tok2Str Token
n) ([TERM_SEQ] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TERM_SEQ]
tseqs) MapSet String Int
forall a b. MapSet a b
MapSet.empty
    TextInfo -> Result TextInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (TextInfo -> Result TextInfo) -> TextInfo -> Result TextInfo
forall a b. (a -> b) -> a -> b
$ [TextInfo] -> TextInfo
unionsTI
             ([TextInfo] -> TextInfo) -> [TextInfo] -> TextInfo
forall a b. (a -> b) -> a -> b
$ ( if PredOrFunc
ty PredOrFunc -> PredOrFunc -> Bool
forall a. Eq a => a -> a -> Bool
== PredOrFunc
Pred
                  then TextInfo
emptyTI { arityPred :: MapSet String Int
arityPred = MapSet String Int
m
                               , boundPred :: MapSet String Int
boundPred = MapSet String Int
m }
                  else TextInfo
emptyTI { arityFunc :: MapSet String Int
arityFunc = MapSet String Int
m
                               , boundFunc :: MapSet String Int
boundFunc = MapSet String Int
m }
                  ) TextInfo -> [TextInfo] -> [TextInfo]
forall a. a -> [a] -> [a]
: [TextInfo]
cti
  _ -> do
    [TextInfo]
cti <- (TERM_SEQ -> Result TextInfo) -> [TERM_SEQ] -> Result [TextInfo]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TERM_SEQ -> Result TextInfo
colTiTrmSeq [TERM_SEQ]
tseqs
    TextInfo
ti <- TERM -> Result TextInfo
colTiTrm TERM
trm
    TextInfo -> Result TextInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (TextInfo -> Result TextInfo)
-> ([TextInfo] -> TextInfo) -> [TextInfo] -> Result TextInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TextInfo] -> TextInfo
unionsTI ([TextInfo] -> Result TextInfo) -> [TextInfo] -> Result TextInfo
forall a b. (a -> b) -> a -> b
$ TextInfo
ti TextInfo -> [TextInfo] -> [TextInfo]
forall a. a -> [a] -> [a]
: [TextInfo]
cti

{- If curried, uncurries term. Otherwise original term returned
removes comments -}

uncurryTermWithArgs :: Cl.TERM -> [Cl.TERM_SEQ] -> (Cl.TERM, [Cl.TERM_SEQ])
uncurryTermWithArgs :: TERM -> [TERM_SEQ] -> (TERM, [TERM_SEQ])
uncurryTermWithArgs trm :: TERM
trm tseqs :: [TERM_SEQ]
tseqs = case TERM
trm of
  Cl.Funct_term t :: TERM
t ts :: [TERM_SEQ]
ts _ -> TERM -> [TERM_SEQ] -> (TERM, [TERM_SEQ])
uncurryTermWithArgs TERM
t ([TERM_SEQ]
ts [TERM_SEQ] -> [TERM_SEQ] -> [TERM_SEQ]
forall a. [a] -> [a] -> [a]
++ [TERM_SEQ]
tseqs)
  Cl.Comment_term t :: TERM
t _ _ -> TERM -> [TERM_SEQ] -> (TERM, [TERM_SEQ])
uncurryTermWithArgs TERM
t [TERM_SEQ]
tseqs
  _ -> (TERM
trm, [TERM_SEQ]
tseqs)