{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/Hybrid2CASL.hs
Copyright   :  nevrenato@gmail.com
License     :  GPLv2 or higher, see LICENSE.txt

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

Comorphism HybridCASL to CASL.
-}

module Comorphisms.Hybrid2CASL
  ( Hybrid2CASL (..)
  ) where

import Logic.Logic
import Logic.Comorphism

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

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

import Hybrid.Logic_Hybrid
import Hybrid.AS_Hybrid
import Hybrid.HybridSign

import CASL.Logic_CASL
import CASL.AS_Basic_CASL
import CASL.Morphism
import CASL.Sign
import CASL.Sublogic as SL


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

-- Just to make things easier to understand
type HForm = HybridFORMULA
type CForm = CASLFORMULA
type CSign = CASLSign


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

instance Comorphism Hybrid2CASL
        Hybrid ()
        H_BASIC_SPEC HForm SYMB_ITEMS SYMB_MAP_ITEMS
        HSign
        HybridMor
        Symbol RawSymbol ()
        CASL
        CASL_Sublogics
        CASLBasicSpec CForm SYMB_ITEMS SYMB_MAP_ITEMS
        CSign
        CASLMor
        Symbol RawSymbol ProofTree where

        sourceLogic :: Hybrid2CASL -> Hybrid
sourceLogic Hybrid2CASL = Hybrid
Hybrid
        sourceSublogic :: Hybrid2CASL -> ()
sourceSublogic Hybrid2CASL = ()
        targetLogic :: Hybrid2CASL -> CASL
targetLogic Hybrid2CASL = CASL
CASL
        mapSublogic :: Hybrid2CASL -> () -> Maybe CASL_Sublogics
mapSublogic Hybrid2CASL _ = CASL_Sublogics -> Maybe CASL_Sublogics
forall a. a -> Maybe a
Just CASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.caslTop
                { cons_features :: SortGenerationFeatures
SL.cons_features = SortGenerationFeatures
SL.emptyMapConsFeature
                , sub_features :: SubsortingFeatures
SL.sub_features = SubsortingFeatures
SL.NoSub
                }
        map_theory :: Hybrid2CASL
-> (HSign, [Named HForm]) -> Result (CSign, [Named CForm])
map_theory Hybrid2CASL = (HSign, [Named HForm]) -> Result (CSign, [Named CForm])
transTheory
        has_model_expansion :: Hybrid2CASL -> Bool
has_model_expansion Hybrid2CASL = Bool
True
        is_weakly_amalgamable :: Hybrid2CASL -> Bool
is_weakly_amalgamable Hybrid2CASL = Bool
True
        is_model_transportable :: Hybrid2CASL -> Bool
is_model_transportable Hybrid2CASL = Bool
True
        isInclusionComorphism :: Hybrid2CASL -> Bool
isInclusionComorphism Hybrid2CASL = Bool
True

{- Translates the given theory in an HybridCASL form to an equivalent
theory in CASL form
Question : Why some sentences are in the sig and other sentences are
in the 2nd argument ? (this is scary)
fs'' is needed for special sentences, refering about datatypes
for which hybridization has nothing to do -}
transTheory :: (HSign, [Named HForm]) -> Result (CSign, [Named CForm])
transTheory :: (HSign, [Named HForm]) -> Result (CSign, [Named CForm])
transTheory (s :: HSign
s, fs :: [Named HForm]
fs) = let
    newSig :: CSign
newSig = HSign -> CSign
transSig HSign
s
    fs' :: [Named CForm]
fs' = (Named HForm -> Named CForm) -> [Named HForm] -> [Named CForm]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((HForm -> CForm) -> Named HForm -> Named CForm
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed HForm -> CForm
trans) [Named HForm]
fs
    fs'' :: [Named CForm]
fs'' = [Named HForm] -> [Named CForm]
dataTrans ([Named HForm]
fs [Named HForm] -> [Named HForm] -> [Named HForm]
forall a. [a] -> [a] -> [a]
++ HSign -> [Named HForm]
forall f e. Sign f e -> [Named (FORMULA f)]
sentences HSign
s)
    newSens :: [Named CForm]
newSens = [Named CForm]
fs' [Named CForm] -> [Named CForm] -> [Named CForm]
forall a. [a] -> [a] -> [a]
++ CSign -> [Named CForm]
forall f e. Sign f e -> [Named (FORMULA f)]
sentences CSign
newSig [Named CForm] -> [Named CForm] -> [Named CForm]
forall a. [a] -> [a] -> [a]
++ [Named CForm]
fs''
    rigidP :: [Named CForm]
rigidP = MapSet PRED_NAME PredType
-> String -> (PRED_NAME -> PredType -> CForm) -> [Named CForm]
forall k a.
Ord k =>
MapSet k a -> String -> (k -> a -> CForm) -> [Named CForm]
applRig (HybridSign -> MapSet PRED_NAME PredType
rigidPreds (HybridSign -> MapSet PRED_NAME PredType)
-> HybridSign -> MapSet PRED_NAME PredType
forall a b. (a -> b) -> a -> b
$ HSign -> HybridSign
forall f e. Sign f e -> e
extendedInfo HSign
s) "RigidPred" PRED_NAME -> PredType -> CForm
gnPCons
    rigidO :: [Named CForm]
rigidO = MapSet PRED_NAME OpType
-> String -> (PRED_NAME -> OpType -> CForm) -> [Named CForm]
forall k a.
Ord k =>
MapSet k a -> String -> (k -> a -> CForm) -> [Named CForm]
applRig (HybridSign -> MapSet PRED_NAME OpType
rigidOps (HybridSign -> MapSet PRED_NAME OpType)
-> HybridSign -> MapSet PRED_NAME OpType
forall a b. (a -> b) -> a -> b
$ HSign -> HybridSign
forall f e. Sign f e -> e
extendedInfo HSign
s) "RigidOp" PRED_NAME -> OpType -> CForm
gnOCons
  in (CSign, [Named CForm]) -> Result (CSign, [Named CForm])
forall (m :: * -> *) a. Monad m => a -> m a
return (CSign
newSig, [Named CForm]
rigidP [Named CForm] -> [Named CForm] -> [Named CForm]
forall a. [a] -> [a] -> [a]
++ [Named CForm]
rigidO [Named CForm] -> [Named CForm] -> [Named CForm]
forall a. [a] -> [a] -> [a]
++ [Named CForm]
newSens)

-- Special formulas not covered by normal hybridization
dataTrans :: [Named HForm] -> [Named CForm]
dataTrans :: [Named HForm] -> [Named CForm]
dataTrans = (Named HForm -> [Named CForm] -> [Named CForm])
-> [Named CForm] -> [Named HForm] -> [Named CForm]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Named HForm -> [Named CForm] -> [Named CForm]
forall f a f.
SenAttr (FORMULA f) a
-> [SenAttr (FORMULA f) a] -> [SenAttr (FORMULA f) a]
f []
        where
        f :: SenAttr (FORMULA f) a
-> [SenAttr (FORMULA f) a] -> [SenAttr (FORMULA f) a]
f a :: SenAttr (FORMULA f) a
a b :: [SenAttr (FORMULA f) a]
b = case SenAttr (FORMULA f) a -> FORMULA f
forall s a. SenAttr s a -> s
sentence SenAttr (FORMULA f) a
a of
            Sort_gen_ax a' :: [Constraint]
a' b' :: Bool
b' -> SenAttr (FORMULA f) a
a { sentence :: FORMULA f
sentence = [Constraint] -> Bool -> FORMULA f
forall f. [Constraint] -> Bool -> FORMULA f
Sort_gen_ax [Constraint]
a' Bool
b' } SenAttr (FORMULA f) a
-> [SenAttr (FORMULA f) a] -> [SenAttr (FORMULA f) a]
forall a. a -> [a] -> [a]
: [SenAttr (FORMULA f) a]
b
            _ -> [SenAttr (FORMULA f) a]
b

transSig :: HSign -> CSign
transSig :: HSign -> CSign
transSig hs :: HSign
hs = let
  workflow :: CSign -> CSign
workflow = HSign -> CSign -> CSign
transSens HSign
hs (CSign -> CSign) -> (CSign -> CSign) -> CSign -> CSign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HSign -> CSign -> CSign
addWrldArg HSign
hs
  workflow' :: CSign -> CSign
workflow' = HSign -> CSign -> CSign
addRels HSign
hs (CSign -> CSign) -> (CSign -> CSign) -> CSign -> CSign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HSign -> CSign -> CSign
addWorlds HSign
hs
  in CSign -> CSign
workflow (CSign -> CSign) -> (CSign -> CSign) -> CSign -> CSign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CSign -> CSign
workflow' (CSign -> CSign) -> CSign -> CSign
forall a b. (a -> b) -> a -> b
$ HSign -> CSign
newSign HSign
hs

{- Creates a new CASL signature based on the hybrid Sig
Also adds the world sort. -}
newSign :: HSign -> CSign
newSign :: HSign -> CSign
newSign hs :: HSign
hs = (() -> CSign
forall e f. e -> Sign f e
emptySign ())
  { sortRel :: Rel PRED_NAME
sortRel = PRED_NAME -> Rel PRED_NAME -> Rel PRED_NAME
forall a. Ord a => a -> Rel a -> Rel a
Rel.insertKey PRED_NAME
worldSort (Rel PRED_NAME -> Rel PRED_NAME) -> Rel PRED_NAME -> Rel PRED_NAME
forall a b. (a -> b) -> a -> b
$ HSign -> Rel PRED_NAME
forall f e. Sign f e -> Rel PRED_NAME
sortRel HSign
hs
  , emptySortSet :: Set PRED_NAME
emptySortSet = HSign -> Set PRED_NAME
forall f e. Sign f e -> Set PRED_NAME
emptySortSet HSign
hs
  , assocOps :: MapSet PRED_NAME OpType
assocOps = HSign -> MapSet PRED_NAME OpType
forall f e. Sign f e -> MapSet PRED_NAME OpType
assocOps HSign
hs
  , varMap :: Map SIMPLE_ID PRED_NAME
varMap = HSign -> Map SIMPLE_ID PRED_NAME
forall f e. Sign f e -> Map SIMPLE_ID PRED_NAME
varMap HSign
hs
  , declaredSymbols :: Set Symbol
declaredSymbols = HSign -> Set Symbol
forall f e. Sign f e -> Set Symbol
declaredSymbols HSign
hs
  , envDiags :: [Diagnosis]
envDiags = HSign -> [Diagnosis]
forall f e. Sign f e -> [Diagnosis]
envDiags HSign
hs
  , annoMap :: AnnoMap
annoMap = HSign -> AnnoMap
forall f e. Sign f e -> AnnoMap
annoMap HSign
hs
  , globAnnos :: GlobalAnnos
globAnnos = HSign -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
globAnnos HSign
hs
  , opMap :: MapSet PRED_NAME OpType
opMap = MapSet PRED_NAME OpType
-> MapSet PRED_NAME OpType -> MapSet PRED_NAME OpType
addOpMapSet (HybridSign -> MapSet PRED_NAME OpType
rigidOps (HybridSign -> MapSet PRED_NAME OpType)
-> HybridSign -> MapSet PRED_NAME OpType
forall a b. (a -> b) -> a -> b
$ HSign -> HybridSign
forall f e. Sign f e -> e
extendedInfo HSign
hs) (HSign -> MapSet PRED_NAME OpType
forall f e. Sign f e -> MapSet PRED_NAME OpType
opMap HSign
hs)
  , predMap :: MapSet PRED_NAME PredType
predMap = MapSet PRED_NAME PredType
-> MapSet PRED_NAME PredType -> MapSet PRED_NAME PredType
addMapSet (HybridSign -> MapSet PRED_NAME PredType
rigidPreds (HybridSign -> MapSet PRED_NAME PredType)
-> HybridSign -> MapSet PRED_NAME PredType
forall a b. (a -> b) -> a -> b
$ HSign -> HybridSign
forall f e. Sign f e -> e
extendedInfo HSign
hs) (HSign -> MapSet PRED_NAME PredType
forall f e. Sign f e -> MapSet PRED_NAME PredType
predMap HSign
hs)
  }

{- | Adds the World constants, based
on the nominals in HSign -}
addWorlds :: HSign -> CSign -> CSign
addWorlds :: HSign -> CSign -> CSign
addWorlds hs :: HSign
hs cs :: CSign
cs =
        let getWorld :: OpType
getWorld = OpKind -> [PRED_NAME] -> PRED_NAME -> OpType
OpType OpKind
Total [] PRED_NAME
worldSort
            s :: HybridSign
s = HSign -> HybridSign
forall f e. Sign f e -> e
extendedInfo HSign
hs
            kl :: [SIMPLE_ID]
kl = Map SIMPLE_ID [AnHybFORM] -> [SIMPLE_ID]
forall k a. Map k a -> [k]
Map.keys (Map SIMPLE_ID [AnHybFORM] -> [SIMPLE_ID])
-> Map SIMPLE_ID [AnHybFORM] -> [SIMPLE_ID]
forall a b. (a -> b) -> a -> b
$ HybridSign -> Map SIMPLE_ID [AnHybFORM]
nomies HybridSign
s
            workflow :: SIMPLE_ID -> PRED_NAME
workflow = String -> PRED_NAME
stringToId (String -> PRED_NAME)
-> (SIMPLE_ID -> String) -> SIMPLE_ID -> PRED_NAME
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ("Wrl_" String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> (SIMPLE_ID -> String) -> SIMPLE_ID -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SIMPLE_ID -> String
tokStr
            il :: [PRED_NAME]
il = (SIMPLE_ID -> PRED_NAME) -> [SIMPLE_ID] -> [PRED_NAME]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SIMPLE_ID -> PRED_NAME
workflow [SIMPLE_ID]
kl
            ins :: MapSet PRED_NAME OpType
ins = (PRED_NAME -> MapSet PRED_NAME OpType -> MapSet PRED_NAME OpType)
-> MapSet PRED_NAME OpType
-> [PRED_NAME]
-> MapSet PRED_NAME OpType
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ k :: PRED_NAME
k m :: MapSet PRED_NAME OpType
m -> PRED_NAME
-> OpType -> MapSet PRED_NAME OpType -> MapSet PRED_NAME OpType
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert PRED_NAME
k OpType
getWorld MapSet PRED_NAME OpType
m) (CSign -> MapSet PRED_NAME OpType
forall f e. Sign f e -> MapSet PRED_NAME OpType
opMap CSign
cs) [PRED_NAME]
il
            in CSign
cs { opMap :: MapSet PRED_NAME OpType
opMap = MapSet PRED_NAME OpType
ins }

{- | Adds the Accessibility relation, based
ono the modalities found in HSign -}
addRels :: HSign -> CSign -> CSign
addRels :: HSign -> CSign -> CSign
addRels hs :: HSign
hs cs :: CSign
cs =
        let accRelT :: PredType
accRelT = [PRED_NAME] -> PredType
PredType [PRED_NAME
worldSort, PRED_NAME
worldSort]
            s :: HybridSign
s = HSign -> HybridSign
forall f e. Sign f e -> e
extendedInfo HSign
hs
            kl :: [SIMPLE_ID]
kl = Map SIMPLE_ID [AnHybFORM] -> [SIMPLE_ID]
forall k a. Map k a -> [k]
Map.keys (Map SIMPLE_ID [AnHybFORM] -> [SIMPLE_ID])
-> Map SIMPLE_ID [AnHybFORM] -> [SIMPLE_ID]
forall a b. (a -> b) -> a -> b
$ HybridSign -> Map SIMPLE_ID [AnHybFORM]
modies HybridSign
s
            il :: [PRED_NAME]
il = (SIMPLE_ID -> PRED_NAME) -> [SIMPLE_ID] -> [PRED_NAME]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> PRED_NAME
stringToId (String -> PRED_NAME)
-> (SIMPLE_ID -> String) -> SIMPLE_ID -> PRED_NAME
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ("Acc_" String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> (SIMPLE_ID -> String) -> SIMPLE_ID -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SIMPLE_ID -> String
tokStr) [SIMPLE_ID]
kl
            ins :: MapSet PRED_NAME PredType
ins = (MapSet PRED_NAME PredType
 -> PRED_NAME -> MapSet PRED_NAME PredType)
-> MapSet PRED_NAME PredType
-> [PRED_NAME]
-> MapSet PRED_NAME PredType
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ m :: MapSet PRED_NAME PredType
m k :: PRED_NAME
k -> PRED_NAME
-> PredType
-> MapSet PRED_NAME PredType
-> MapSet PRED_NAME PredType
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert PRED_NAME
k PredType
accRelT MapSet PRED_NAME PredType
m) (CSign -> MapSet PRED_NAME PredType
forall f e. Sign f e -> MapSet PRED_NAME PredType
predMap CSign
cs) [PRED_NAME]
il
            in CSign
cs { predMap :: MapSet PRED_NAME PredType
predMap = MapSet PRED_NAME PredType
ins }

{- | Adds one argument of type World to all preds and ops
definitions in an hybrid signature and passes them to a caslsig -}
addWrldArg :: HSign -> CSign -> CSign
addWrldArg :: HSign -> CSign -> CSign
addWrldArg hs :: HSign
hs cs :: CSign
cs = let
    f :: OpType -> OpType
f (OpType a :: OpKind
a b :: [PRED_NAME]
b c :: PRED_NAME
c) = OpKind -> [PRED_NAME] -> PRED_NAME -> OpType
OpType OpKind
a (PRED_NAME
worldSort PRED_NAME -> [PRED_NAME] -> [PRED_NAME]
forall a. a -> [a] -> [a]
: [PRED_NAME]
b) PRED_NAME
c
    g :: PredType -> PredType
g (PredType a :: [PRED_NAME]
a) = [PRED_NAME] -> PredType
PredType (PRED_NAME
worldSort PRED_NAME -> [PRED_NAME] -> [PRED_NAME]
forall a. a -> [a] -> [a]
: [PRED_NAME]
a)
    ops :: MapSet PRED_NAME OpType
ops = MapSet PRED_NAME OpType
-> MapSet PRED_NAME OpType -> MapSet PRED_NAME OpType
addOpMapSet (HybridSign -> MapSet PRED_NAME OpType
rigidOps (HybridSign -> MapSet PRED_NAME OpType)
-> HybridSign -> MapSet PRED_NAME OpType
forall a b. (a -> b) -> a -> b
$ HSign -> HybridSign
forall f e. Sign f e -> e
extendedInfo HSign
hs) (HSign -> MapSet PRED_NAME OpType
forall f e. Sign f e -> MapSet PRED_NAME OpType
opMap HSign
hs)
    preds :: MapSet PRED_NAME PredType
preds = MapSet PRED_NAME PredType
-> MapSet PRED_NAME PredType -> MapSet PRED_NAME PredType
addMapSet (HybridSign -> MapSet PRED_NAME PredType
rigidPreds (HybridSign -> MapSet PRED_NAME PredType)
-> HybridSign -> MapSet PRED_NAME PredType
forall a b. (a -> b) -> a -> b
$ HSign -> HybridSign
forall f e. Sign f e -> e
extendedInfo HSign
hs) (HSign -> MapSet PRED_NAME PredType
forall f e. Sign f e -> MapSet PRED_NAME PredType
predMap HSign
hs)
    ks :: [PRED_NAME]
ks = Set PRED_NAME -> [PRED_NAME]
forall a. Set a -> [a]
Set.elems (Set PRED_NAME -> [PRED_NAME]) -> Set PRED_NAME -> [PRED_NAME]
forall a b. (a -> b) -> a -> b
$ MapSet PRED_NAME OpType -> Set PRED_NAME
forall a b. MapSet a b -> Set a
MapSet.keysSet MapSet PRED_NAME OpType
ops
    ks' :: [PRED_NAME]
ks' = Set PRED_NAME -> [PRED_NAME]
forall a. Set a -> [a]
Set.elems (Set PRED_NAME -> [PRED_NAME]) -> Set PRED_NAME -> [PRED_NAME]
forall a b. (a -> b) -> a -> b
$ MapSet PRED_NAME PredType -> Set PRED_NAME
forall a b. MapSet a b -> Set a
MapSet.keysSet MapSet PRED_NAME PredType
preds
  in CSign
cs
    { opMap :: MapSet PRED_NAME OpType
opMap = (PRED_NAME -> MapSet PRED_NAME OpType -> MapSet PRED_NAME OpType)
-> MapSet PRED_NAME OpType
-> [PRED_NAME]
-> MapSet PRED_NAME OpType
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Set OpType -> Set OpType)
-> PRED_NAME -> MapSet PRED_NAME OpType -> MapSet PRED_NAME OpType
forall a b.
(Ord a, Ord b) =>
(Set b -> Set b) -> a -> MapSet a b -> MapSet a b
MapSet.update ((OpType -> OpType) -> Set OpType -> Set OpType
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map OpType -> OpType
f)) (CSign -> MapSet PRED_NAME OpType
forall f e. Sign f e -> MapSet PRED_NAME OpType
opMap CSign
cs) [PRED_NAME]
ks
    , predMap :: MapSet PRED_NAME PredType
predMap = (PRED_NAME
 -> MapSet PRED_NAME PredType -> MapSet PRED_NAME PredType)
-> MapSet PRED_NAME PredType
-> [PRED_NAME]
-> MapSet PRED_NAME PredType
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Set PredType -> Set PredType)
-> PRED_NAME
-> MapSet PRED_NAME PredType
-> MapSet PRED_NAME PredType
forall a b.
(Ord a, Ord b) =>
(Set b -> Set b) -> a -> MapSet a b -> MapSet a b
MapSet.update ((PredType -> PredType) -> Set PredType -> Set PredType
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map PredType -> PredType
g)) (CSign -> MapSet PRED_NAME PredType
forall f e. Sign f e -> MapSet PRED_NAME PredType
predMap CSign
cs) [PRED_NAME]
ks'
    }

{- Translates all hybridformulas in a hybridSig to caslformulas
Ones are in the declaration of nominals and modalities (however
for nows that is forbidden to happen)
The others come from the casl sig -}
transSens :: HSign -> CSign -> CSign
transSens :: HSign -> CSign -> CSign
transSens hs :: HSign
hs cs :: CSign
cs = let
    mods :: [[AnHybFORM]]
mods = Map SIMPLE_ID [AnHybFORM] -> [[AnHybFORM]]
forall k a. Map k a -> [a]
Map.elems (HybridSign -> Map SIMPLE_ID [AnHybFORM]
modies (HybridSign -> Map SIMPLE_ID [AnHybFORM])
-> HybridSign -> Map SIMPLE_ID [AnHybFORM]
forall a b. (a -> b) -> a -> b
$ HSign -> HybridSign
forall f e. Sign f e -> e
extendedInfo HSign
hs)
    noms :: [[AnHybFORM]]
noms = Map SIMPLE_ID [AnHybFORM] -> [[AnHybFORM]]
forall k a. Map k a -> [a]
Map.elems (HybridSign -> Map SIMPLE_ID [AnHybFORM]
nomies (HybridSign -> Map SIMPLE_ID [AnHybFORM])
-> HybridSign -> Map SIMPLE_ID [AnHybFORM]
forall a b. (a -> b) -> a -> b
$ HSign -> HybridSign
forall f e. Sign f e -> e
extendedInfo HSign
hs)
    fs :: [AnHybFORM]
fs = [[AnHybFORM]] -> [AnHybFORM]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[AnHybFORM]] -> [AnHybFORM]) -> [[AnHybFORM]] -> [AnHybFORM]
forall a b. (a -> b) -> a -> b
$ [[AnHybFORM]]
mods [[AnHybFORM]] -> [[AnHybFORM]] -> [[AnHybFORM]]
forall a. [a] -> [a] -> [a]
++ [[AnHybFORM]]
noms
    workflow :: AnHybFORM -> Named CForm
workflow = String -> CForm -> Named CForm
forall a s. a -> s -> SenAttr s a
makeNamed "" (CForm -> Named CForm)
-> (AnHybFORM -> CForm) -> AnHybFORM -> Named CForm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HForm -> CForm
trans (HForm -> CForm) -> (AnHybFORM -> HForm) -> AnHybFORM -> CForm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnHybFORM -> HForm
forall a. Annoted a -> a
item
    fs' :: [Named CForm]
fs' = (AnHybFORM -> Named CForm) -> [AnHybFORM] -> [Named CForm]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AnHybFORM -> Named CForm
workflow [AnHybFORM]
fs
    fs'' :: [Named CForm]
fs'' = (Named HForm -> Named CForm) -> [Named HForm] -> [Named CForm]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((HForm -> CForm) -> Named HForm -> Named CForm
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed HForm -> CForm
trans) (HSign -> [Named HForm]
forall f e. Sign f e -> [Named (FORMULA f)]
sentences HSign
hs)
  in CSign
cs { sentences :: [Named CForm]
sentences = [Named CForm]
fs' [Named CForm] -> [Named CForm] -> [Named CForm]
forall a. [a] -> [a] -> [a]
++ [Named CForm]
fs'' }

-- Translates an HybridCASL formula to CASL formula
trans :: HForm -> CForm
trans :: HForm -> CForm
trans = let w :: SIMPLE_ID
w = String -> SIMPLE_ID
mkSimpleId "world"
            vars :: VAR_DECL
vars = SIMPLE_ID -> PRED_NAME -> VAR_DECL
mkVarDecl SIMPLE_ID
w PRED_NAME
worldSort
        in [VAR_DECL] -> CForm -> CForm
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL
vars] (CForm -> CForm) -> (HForm -> CForm) -> HForm -> CForm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mode -> [String] -> HForm -> CForm
trForm (SIMPLE_ID -> Mode
QtM SIMPLE_ID
w) []

{- | Formula translator
The 2nd argument is used to store the reserved words -}
trForm :: Mode -> [String] -> HForm -> CForm
trForm :: Mode -> [String] -> HForm -> CForm
trForm w :: Mode
w s :: [String]
s b :: HForm
b = case HForm
b of
    ExtFORMULA f :: H_FORMULA
f -> Mode -> [String] -> H_FORMULA -> CForm
alpha Mode
w [String]
s H_FORMULA
f
    Junction j :: Junctor
j fs :: [HForm]
fs r :: Range
r -> Junctor -> [CForm] -> Range -> CForm
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
j ((HForm -> CForm) -> [HForm] -> [CForm]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Mode -> [String] -> HForm -> CForm
trForm Mode
w [String]
s) [HForm]
fs) Range
r
    Relation f :: HForm
f r :: Relation
r f' :: HForm
f' q :: Range
q -> CForm -> Relation -> CForm -> Range -> CForm
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation (Mode -> [String] -> HForm -> CForm
trForm Mode
w [String]
s HForm
f) Relation
r (Mode -> [String] -> HForm -> CForm
trForm Mode
w [String]
s HForm
f') Range
q
    Negation f :: HForm
f _ -> CForm -> CForm
forall f. FORMULA f -> FORMULA f
mkNeg (CForm -> CForm) -> CForm -> CForm
forall a b. (a -> b) -> a -> b
$ Mode -> [String] -> HForm -> CForm
trForm Mode
w [String]
s HForm
f
    Predication p :: PRED_SYMB
p l :: [TERM H_FORMULA]
l _ -> PRED_SYMB -> [TERM ()] -> CForm
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication (PRED_SYMB -> PRED_SYMB
mkPName PRED_SYMB
p) ([TERM ()] -> CForm) -> [TERM ()] -> CForm
forall a b. (a -> b) -> a -> b
$ Mode -> [String] -> [TERM H_FORMULA] -> [TERM ()]
trTerms Mode
w [String]
s [TERM H_FORMULA]
l
    Quantification q :: QUANTIFIER
q l :: [VAR_DECL]
l f :: HForm
f r :: Range
r -> QUANTIFIER -> [VAR_DECL] -> CForm -> Range -> CForm
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
l (Mode -> [String] -> HForm -> CForm
trForm Mode
w [String]
s HForm
f) Range
r
    Definedness t :: TERM H_FORMULA
t _ -> TERM () -> Range -> CForm
forall f. TERM f -> Range -> FORMULA f
Definedness (Mode -> [String] -> TERM H_FORMULA -> TERM ()
trTerm Mode
w [String]
s TERM H_FORMULA
t) Range
nullRange
    Atom a :: Bool
a r :: Range
r -> Bool -> Range -> CForm
forall f. Bool -> Range -> FORMULA f
Atom Bool
a Range
r
    _ -> String -> CForm
forall a. HasCallStack => String -> a
error "Hybrid2CASL.trForm"

-- | Alpha function, translates pure Hybrid Formulas
alpha :: Mode -> [String] -> H_FORMULA -> CForm
alpha :: Mode -> [String] -> H_FORMULA -> CForm
alpha w :: Mode
w s :: [String]
s b :: H_FORMULA
b = case H_FORMULA
b of
    Here n :: NOMINAL
n _ -> TERM () -> TERM () -> CForm
forall f. TERM f -> TERM f -> FORMULA f
mkStEq (Either Mode NOMINAL -> [String] -> TERM ()
mkArg (NOMINAL -> Either Mode NOMINAL
forall a b. b -> Either a b
Right NOMINAL
n) [String]
s) (TERM () -> CForm) -> TERM () -> CForm
forall a b. (a -> b) -> a -> b
$ case Mode
w of
         QtM wm :: SIMPLE_ID
wm -> SIMPLE_ID -> PRED_NAME -> TERM ()
forall f. SIMPLE_ID -> PRED_NAME -> TERM f
mkVarTerm SIMPLE_ID
wm PRED_NAME
worldSort
         _ -> Either Mode NOMINAL -> [String] -> TERM ()
mkArg (Mode -> Either Mode NOMINAL
forall a b. a -> Either a b
Left Mode
w) [String]
s
    BoxOrDiamond True m :: MODALITY
m f :: HForm
f _ -> Mode -> MODALITY -> [String] -> HForm -> CForm
trBox Mode
w MODALITY
m [String]
s HForm
f
    BoxOrDiamond False m :: MODALITY
m f :: HForm
f _ -> Mode -> [String] -> HForm -> CForm
trForm Mode
w [String]
s (HForm -> CForm) -> HForm -> CForm
forall a b. (a -> b) -> a -> b
$ MODALITY -> HForm -> HForm
toBox MODALITY
m HForm
f
    At (Simple_nom n :: SIMPLE_ID
n) f :: HForm
f _ -> Mode -> [String] -> HForm -> CForm
trForm (SIMPLE_ID -> Mode
AtM SIMPLE_ID
n) [String]
s HForm
f
    Univ n :: NOMINAL
n f :: HForm
f _ -> Mode -> NOMINAL -> [String] -> HForm -> CForm
trForall Mode
w NOMINAL
n [String]
s HForm
f
    Exist n :: NOMINAL
n f :: HForm
f _ -> CForm -> CForm
forall f. FORMULA f -> FORMULA f
mkNeg (CForm -> CForm) -> CForm -> CForm
forall a b. (a -> b) -> a -> b
$ Mode -> NOMINAL -> [String] -> HForm -> CForm
trForall Mode
w NOMINAL
n [String]
s (HForm -> HForm
forall f. FORMULA f -> FORMULA f
mkNeg HForm
f)
  where
    toBox :: MODALITY -> HForm -> HForm
toBox m :: MODALITY
m f :: HForm
f = HForm -> HForm
forall f. FORMULA f -> FORMULA f
mkNeg (HForm -> HForm) -> (H_FORMULA -> HForm) -> H_FORMULA -> HForm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. H_FORMULA -> HForm
forall f. f -> FORMULA f
ExtFORMULA (H_FORMULA -> HForm) -> H_FORMULA -> HForm
forall a b. (a -> b) -> a -> b
$ Bool -> MODALITY -> HForm -> Range -> H_FORMULA
BoxOrDiamond Bool
True MODALITY
m (HForm -> HForm
forall f. FORMULA f -> FORMULA f
mkNeg HForm
f) Range
nullRange

-- | Function that takes care of formulas of box type
trBox :: Mode -> MODALITY -> [String] -> HForm -> CForm
trBox :: Mode -> MODALITY -> [String] -> HForm -> CForm
trBox m :: Mode
m (Simple_mod m' :: SIMPLE_ID
m') s :: [String]
s f :: HForm
f = CForm -> CForm
forall f. FORMULA f -> FORMULA f
quant (CForm -> CForm) -> CForm -> CForm
forall a b. (a -> b) -> a -> b
$ CForm -> CForm -> CForm
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl CForm
prd (CForm -> CForm) -> CForm -> CForm
forall a b. (a -> b) -> a -> b
$ Mode -> [String] -> HForm -> CForm
trForm (SIMPLE_ID -> Mode
QtM SIMPLE_ID
v) [String]
ss HForm
f
  where
    quant :: FORMULA f -> FORMULA f
quant = [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL
var]
    var :: VAR_DECL
var = SIMPLE_ID -> PRED_NAME -> VAR_DECL
mkVarDecl SIMPLE_ID
v PRED_NAME
worldSort
    v :: SIMPLE_ID
v = String -> SIMPLE_ID
mkSimpleId (String -> SIMPLE_ID) -> String -> SIMPLE_ID
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall a. [a] -> a
head [String]
ss
    ss :: [String]
ss = [String] -> [String]
newVarName [String]
s
    prd :: CForm
prd = PRED_SYMB -> [TERM ()] -> CForm
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
predN ([TERM ()] -> CForm) -> [TERM ()] -> CForm
forall a b. (a -> b) -> a -> b
$ Mode -> [TERM ()]
predA Mode
m
    predN :: PRED_SYMB
predN = SIMPLE_ID -> PRED_TYPE -> PRED_SYMB
forall a. Show a => a -> PRED_TYPE -> PRED_SYMB
qp SIMPLE_ID
m' PRED_TYPE
t
    predA :: Mode -> [TERM ()]
predA w :: Mode
w = [Either Mode NOMINAL -> [String] -> TERM ()
mkArg (Mode -> Either Mode NOMINAL
forall a b. a -> Either a b
Left Mode
w) [String]
s, Either Mode NOMINAL -> [String] -> TERM ()
mkArg (Mode -> Either Mode NOMINAL
forall a b. a -> Either a b
Left (SIMPLE_ID -> Mode
QtM SIMPLE_ID
v)) [String]
s]
    qp :: a -> PRED_TYPE -> PRED_SYMB
qp x :: a
x = PRED_NAME -> PRED_TYPE -> PRED_SYMB
mkQualPred (String -> PRED_NAME
stringToId (String -> PRED_NAME) -> ShowS -> String -> PRED_NAME
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ("Acc_" String -> ShowS
forall a. [a] -> [a] -> [a]
++) (String -> PRED_NAME) -> String -> PRED_NAME
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
x)
    t :: PRED_TYPE
t = [PRED_NAME] -> Range -> PRED_TYPE
Pred_type [PRED_NAME
worldSort, PRED_NAME
worldSort] Range
nullRange
trBox _ _ _ _ = CForm
forall f. FORMULA f
trueForm

-- translation function for the quantification of nominals case
trForall :: Mode -> NOMINAL -> [String] -> HForm -> CForm
trForall :: Mode -> NOMINAL -> [String] -> HForm -> CForm
trForall w :: Mode
w (Simple_nom a :: SIMPLE_ID
a) s :: [String]
s f :: HForm
f = [VAR_DECL] -> CForm -> CForm
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [SIMPLE_ID -> PRED_NAME -> VAR_DECL
mkVarDecl SIMPLE_ID
a PRED_NAME
worldSort]
  (CForm -> CForm) -> CForm -> CForm
forall a b. (a -> b) -> a -> b
$ Mode -> [String] -> HForm -> CForm
trForm Mode
w (SIMPLE_ID -> String
forall a. Show a => a -> String
show SIMPLE_ID
a String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
s) HForm
f

-- Function that translates a list of hybrid terms to casl terms
trTerms :: Mode -> [String] -> [TERM H_FORMULA] -> [TERM ()]
trTerms :: Mode -> [String] -> [TERM H_FORMULA] -> [TERM ()]
trTerms m :: Mode
m s :: [String]
s l :: [TERM H_FORMULA]
l = Either Mode NOMINAL -> [String] -> TERM ()
mkArg (Mode -> Either Mode NOMINAL
forall a b. a -> Either a b
Left Mode
m) [String]
s TERM () -> [TERM ()] -> [TERM ()]
forall a. a -> [a] -> [a]
: (TERM H_FORMULA -> TERM ()) -> [TERM H_FORMULA] -> [TERM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Mode -> [String] -> TERM H_FORMULA -> TERM ()
trTerm Mode
m [String]
s) [TERM H_FORMULA]
l

-- Function that translates hybrid term to casl term
trTerm :: Mode -> [String] -> TERM H_FORMULA -> TERM ()
trTerm :: Mode -> [String] -> TERM H_FORMULA -> TERM ()
trTerm m :: Mode
m s :: [String]
s t :: TERM H_FORMULA
t = case TERM H_FORMULA
t of
  Qual_var v :: SIMPLE_ID
v s' :: PRED_NAME
s' x :: Range
x -> SIMPLE_ID -> PRED_NAME -> Range -> TERM ()
forall f. SIMPLE_ID -> PRED_NAME -> Range -> TERM f
Qual_var SIMPLE_ID
v PRED_NAME
s' Range
x
  Application o :: OP_SYMB
o l :: [TERM H_FORMULA]
l r :: Range
r -> OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (OP_SYMB -> OP_SYMB
mkOName OP_SYMB
o) (Mode -> [String] -> [TERM H_FORMULA] -> [TERM ()]
trTerms Mode
m [String]
s [TERM H_FORMULA]
l) Range
r
  Sorted_term t' :: TERM H_FORMULA
t' s' :: PRED_NAME
s' r :: Range
r -> TERM () -> PRED_NAME -> Range -> TERM ()
forall f. TERM f -> PRED_NAME -> Range -> TERM f
Sorted_term (Mode -> [String] -> TERM H_FORMULA -> TERM ()
trTerm Mode
m [String]
s TERM H_FORMULA
t') PRED_NAME
s' Range
r
  _ -> String -> TERM ()
forall a. HasCallStack => String -> a
error "Hybrid2CASL.trTerm"


-- **** Auxiliar functions and datatype ****

-- The world sort type
worldSort :: SORT
worldSort :: PRED_NAME
worldSort = String -> PRED_NAME
stringToId "World"

mkPName :: PRED_SYMB -> PRED_SYMB
mkPName :: PRED_SYMB -> PRED_SYMB
mkPName ~(Qual_pred_name n :: PRED_NAME
n t :: PRED_TYPE
t _) = PRED_NAME -> PRED_TYPE -> PRED_SYMB
mkQualPred PRED_NAME
n (PRED_TYPE -> PRED_TYPE
f PRED_TYPE
t)
        where f :: PRED_TYPE -> PRED_TYPE
f (Pred_type l :: [PRED_NAME]
l r :: Range
r) = [PRED_NAME] -> Range -> PRED_TYPE
Pred_type (PRED_NAME
worldSort PRED_NAME -> [PRED_NAME] -> [PRED_NAME]
forall a. a -> [a] -> [a]
: [PRED_NAME]
l) Range
r

mkOName :: OP_SYMB -> OP_SYMB
mkOName :: OP_SYMB -> OP_SYMB
mkOName ~(Qual_op_name n :: PRED_NAME
n t :: OP_TYPE
t _) = PRED_NAME -> OP_TYPE -> OP_SYMB
mkQualOp PRED_NAME
n (OP_TYPE -> OP_TYPE
f OP_TYPE
t)
        where f :: OP_TYPE -> OP_TYPE
f (Op_type o :: OpKind
o l :: [PRED_NAME]
l s :: PRED_NAME
s r :: Range
r) = OpKind -> [PRED_NAME] -> PRED_NAME -> Range -> OP_TYPE
Op_type OpKind
o (PRED_NAME
worldSort PRED_NAME -> [PRED_NAME] -> [PRED_NAME]
forall a. a -> [a] -> [a]
: [PRED_NAME]
l) PRED_NAME
s Range
r

{- Function that will decide how to create a new argument
That argument can be a variable or a nominal (constant) -}
mkArg :: Either Mode NOMINAL -> [String] -> TERM ()
mkArg :: Either Mode NOMINAL -> [String] -> TERM ()
mkArg a :: Either Mode NOMINAL
a l :: [String]
l = case Either Mode NOMINAL
a of
                Left (QtM w :: SIMPLE_ID
w) -> SIMPLE_ID -> TERM ()
forall f. SIMPLE_ID -> TERM f
vt SIMPLE_ID
w
                Left (AtM w :: SIMPLE_ID
w) -> (SIMPLE_ID -> String) -> SIMPLE_ID -> TERM ()
forall f. (SIMPLE_ID -> String) -> SIMPLE_ID -> TERM f
ch SIMPLE_ID -> String
tokStr SIMPLE_ID
w
                Right (Simple_nom n :: SIMPLE_ID
n) -> (SIMPLE_ID -> String) -> SIMPLE_ID -> TERM ()
forall f. (SIMPLE_ID -> String) -> SIMPLE_ID -> TERM f
ch SIMPLE_ID -> String
forall a. Show a => a -> String
show SIMPLE_ID
n
              where
                vt :: SIMPLE_ID -> TERM f
vt x :: SIMPLE_ID
x = SIMPLE_ID -> PRED_NAME -> TERM f
forall f. SIMPLE_ID -> PRED_NAME -> TERM f
mkVarTerm SIMPLE_ID
x PRED_NAME
worldSort
                ap :: a -> TERM f
ap x :: a
x = OP_SYMB -> [TERM f] -> TERM f
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl (a -> OP_TYPE -> OP_SYMB
forall a. Show a => a -> OP_TYPE -> OP_SYMB
qo a
x OP_TYPE
t) []
                ch :: (SIMPLE_ID -> String) -> SIMPLE_ID -> TERM f
ch f :: SIMPLE_ID -> String
f x :: SIMPLE_ID
x = if SIMPLE_ID -> String
f SIMPLE_ID
x String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
l then SIMPLE_ID -> TERM f
forall f. SIMPLE_ID -> TERM f
vt SIMPLE_ID
x else SIMPLE_ID -> TERM f
forall a f. Show a => a -> TERM f
ap SIMPLE_ID
x
                qo :: a -> OP_TYPE -> OP_SYMB
qo x :: a
x = PRED_NAME -> OP_TYPE -> OP_SYMB
mkQualOp (PRED_NAME -> OP_TYPE -> OP_SYMB)
-> PRED_NAME -> OP_TYPE -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ String -> PRED_NAME
stringToId (String -> PRED_NAME) -> ShowS -> String -> PRED_NAME
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ("Wrl_" String -> ShowS
forall a. [a] -> [a] -> [a]
++) (String -> PRED_NAME) -> String -> PRED_NAME
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
x
                t :: OP_TYPE
t = OpKind -> [PRED_NAME] -> PRED_NAME -> Range -> OP_TYPE
Op_type OpKind
Total [] PRED_NAME
worldSort Range
nullRange


-- Create a new variable name new in the formula
newVarName :: [String] -> [String]
newVarName :: [String] -> [String]
newVarName xs :: [String]
xs = ("world" String -> ShowS
forall a. [a] -> [a] -> [a]
++) (Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ [String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
xs) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
xs

{- | Auxiliar datatype to determine wich is the argument of alpha
Quantified Mode or At mode -}
data Mode = QtM VAR | AtM SIMPLE_ID

-- **** End of auxiliar functions and datatypes section ****************

-- ----- Generation of constraints associated with rigid designators

toName :: (Functor f) => String -> f a -> f (Named a)
toName :: String -> f a -> f (Named a)
toName s :: String
s = (a -> Named a) -> f a -> f (Named a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> Named a) -> f a -> f (Named a))
-> (a -> Named a) -> f a -> f (Named a)
forall a b. (a -> b) -> a -> b
$ String -> a -> Named a
forall a s. a -> s -> SenAttr s a
makeNamed String
s

{- Adds the constraints associated with the rigidity
of predicates or operations. -}
applRig :: (Ord k) => MapSet.MapSet k a ->
           String ->
           (k -> a -> CForm) ->
           [Named CForm]
applRig :: MapSet k a -> String -> (k -> a -> CForm) -> [Named CForm]
applRig m :: MapSet k a
m s :: String
s f :: k -> a -> CForm
f = String -> [CForm] -> [Named CForm]
forall (f :: * -> *) a. Functor f => String -> f a -> f (Named a)
toName String
s ([CForm] -> [Named CForm]) -> [CForm] -> [Named CForm]
forall a b. (a -> b) -> a -> b
$ [k] -> (k -> a -> CForm) -> MapSet k a -> [CForm]
forall k a.
Ord k =>
[k] -> (k -> a -> CForm) -> MapSet k a -> [CForm]
glueDs [k]
ks k -> a -> CForm
f MapSet k a
m
        where ks :: [k]
ks = Set k -> [k]
forall a. Set a -> [a]
Set.elems (Set k -> [k]) -> Set k -> [k]
forall a b. (a -> b) -> a -> b
$ MapSet k a -> Set k
forall a b. MapSet a b -> Set a
MapSet.keysSet MapSet k a
m

{- Given a list of designators, generates the rigidity constraints
associated, and concats them into a single list -}
glueDs :: (Ord k) => [k] ->
          (k -> a -> CForm) ->
          MapSet.MapSet k a ->
          [CForm]
glueDs :: [k] -> (k -> a -> CForm) -> MapSet k a -> [CForm]
glueDs ks :: [k]
ks f :: k -> a -> CForm
f m :: MapSet k a
m = [[CForm]] -> [CForm]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[CForm]] -> [CForm]) -> [[CForm]] -> [CForm]
forall a b. (a -> b) -> a -> b
$ (k -> [[CForm]] -> [[CForm]]) -> [[CForm]] -> [k] -> [[CForm]]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ a :: k
a b :: [[CForm]]
b -> k -> [CForm]
g k
a [CForm] -> [[CForm]] -> [[CForm]]
forall a. a -> [a] -> [a]
: [[CForm]]
b) [] [k]
ks
       where g :: k -> [CForm]
g k :: k
k = k -> Set a -> (k -> a -> CForm) -> [CForm]
forall k a. k -> Set a -> (k -> a -> CForm) -> [CForm]
glueDe k
k (k -> MapSet k a -> Set a
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup k
k MapSet k a
m) k -> a -> CForm
f

{- Given a single designator, genereates the rigidity constraints
associated, and joins them into a single list -}
glueDe :: k -> Set.Set a -> (k -> a -> CForm) -> [CForm]
glueDe :: k -> Set a -> (k -> a -> CForm) -> [CForm]
glueDe n :: k
n s :: Set a
s f :: k -> a -> CForm
f = (a -> [CForm] -> [CForm]) -> [CForm] -> [a] -> [CForm]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ a :: a
a b :: [CForm]
b -> k -> a -> CForm
f k
n a
a CForm -> [CForm] -> [CForm]
forall a. a -> [a] -> [a]
: [CForm]
b) [] ([a] -> [CForm]) -> [a] -> [CForm]
forall a b. (a -> b) -> a -> b
$ Set a -> [a]
forall a. Set a -> [a]
Set.elems Set a
s

{- Generates a rigid constraint from a single pred name and type
We add the extra world argument in mkPredType so that it coincides
with the later translated predicate definition -}
gnPCons :: PRED_NAME -> PredType -> CForm
gnPCons :: PRED_NAME -> PredType -> CForm
gnPCons n :: PRED_NAME
n (PredType ts :: [PRED_NAME]
ts) = [VAR_DECL] -> CForm -> CForm
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL]
decls (CForm -> CForm) -> CForm -> CForm
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> CForm -> CForm
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL]
wA (CForm -> CForm) -> CForm -> CForm
forall a b. (a -> b) -> a -> b
$ CForm -> CForm -> CForm
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl CForm
forall f. FORMULA f
f1 CForm
forall f. FORMULA f
f2
        where f1 :: FORMULA f
f1 = PRED_SYMB -> [TERM f] -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
predName ([TERM f] -> FORMULA f) -> [TERM f] -> FORMULA f
forall a b. (a -> b) -> a -> b
$ VAR_DECL -> [TERM f]
forall f. VAR_DECL -> [TERM f]
terms VAR_DECL
w1
              f2 :: FORMULA f
f2 = PRED_SYMB -> [TERM f] -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
predName ([TERM f] -> FORMULA f) -> [TERM f] -> FORMULA f
forall a b. (a -> b) -> a -> b
$ VAR_DECL -> [TERM f]
forall f. VAR_DECL -> [TERM f]
terms VAR_DECL
w2
              decls :: [VAR_DECL]
decls = [PRED_NAME] -> [VAR_DECL]
fromSort [PRED_NAME]
ts
              terms :: VAR_DECL -> [TERM f]
terms x :: VAR_DECL
x = [VAR_DECL] -> [TERM f]
forall f. [VAR_DECL] -> [TERM f]
fromDecls ([VAR_DECL] -> [TERM f]) -> [VAR_DECL] -> [TERM f]
forall a b. (a -> b) -> a -> b
$ VAR_DECL
x VAR_DECL -> [VAR_DECL] -> [VAR_DECL]
forall a. a -> [a] -> [a]
: [VAR_DECL]
decls
              predName :: PRED_SYMB
predName = PRED_NAME -> PRED_TYPE -> PRED_SYMB
mkQualPred PRED_NAME
n (PRED_TYPE -> PRED_SYMB) -> PRED_TYPE -> PRED_SYMB
forall a b. (a -> b) -> a -> b
$ [PRED_NAME] -> PRED_TYPE
mkPredType [PRED_NAME]
ts
              mkPredType :: [PRED_NAME] -> PRED_TYPE
mkPredType x :: [PRED_NAME]
x = [PRED_NAME] -> Range -> PRED_TYPE
Pred_type (PRED_NAME
worldSort PRED_NAME -> [PRED_NAME] -> [PRED_NAME]
forall a. a -> [a] -> [a]
: [PRED_NAME]
x) Range
nullRange

gnOCons :: OP_NAME -> OpType -> CForm
gnOCons :: PRED_NAME -> OpType -> CForm
gnOCons n :: PRED_NAME
n (OpType o :: OpKind
o ts :: [PRED_NAME]
ts t :: PRED_NAME
t) = [VAR_DECL] -> CForm -> CForm
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL]
decls (CForm -> CForm) -> CForm -> CForm
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> CForm -> CForm
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL]
wA CForm
forall f. FORMULA f
f
          where f :: FORMULA f
f = TERM f -> TERM f -> FORMULA f
forall f. TERM f -> TERM f -> FORMULA f
mkStEq (OP_SYMB -> [TERM f] -> TERM f
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
opName ([TERM f] -> TERM f) -> [TERM f] -> TERM f
forall a b. (a -> b) -> a -> b
$ VAR_DECL -> [TERM f]
forall f. VAR_DECL -> [TERM f]
terms VAR_DECL
w1) TERM f
forall f. TERM f
t2
                t2 :: TERM f
t2 = OP_SYMB -> [TERM f] -> TERM f
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
opName ([TERM f] -> TERM f) -> [TERM f] -> TERM f
forall a b. (a -> b) -> a -> b
$ VAR_DECL -> [TERM f]
forall f. VAR_DECL -> [TERM f]
terms VAR_DECL
w2
                decls :: [VAR_DECL]
decls = [PRED_NAME] -> [VAR_DECL]
fromSort [PRED_NAME]
ts
                terms :: VAR_DECL -> [TERM f]
terms x :: VAR_DECL
x = [VAR_DECL] -> [TERM f]
forall f. [VAR_DECL] -> [TERM f]
fromDecls ([VAR_DECL] -> [TERM f]) -> [VAR_DECL] -> [TERM f]
forall a b. (a -> b) -> a -> b
$ VAR_DECL
x VAR_DECL -> [VAR_DECL] -> [VAR_DECL]
forall a. a -> [a] -> [a]
: [VAR_DECL]
decls
                opName :: OP_SYMB
opName = PRED_NAME -> OP_TYPE -> OP_SYMB
mkQualOp PRED_NAME
n (OP_TYPE -> OP_SYMB) -> OP_TYPE -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ OpKind -> [PRED_NAME] -> PRED_NAME -> OP_TYPE
mkOpType OpKind
o (PRED_NAME
worldSort PRED_NAME -> [PRED_NAME] -> [PRED_NAME]
forall a. a -> [a] -> [a]
: [PRED_NAME]
ts) PRED_NAME
t
                mkOpType :: OpKind -> [PRED_NAME] -> PRED_NAME -> OP_TYPE
mkOpType x :: OpKind
x y :: [PRED_NAME]
y z :: PRED_NAME
z = OpKind -> [PRED_NAME] -> PRED_NAME -> Range -> OP_TYPE
Op_type OpKind
x [PRED_NAME]
y PRED_NAME
z Range
nullRange


{- The next functions are auxiliar. They are need for generating the
proper variables/terms for the quantifiers,predications and operations. -}
w1 :: VAR_DECL
w1 :: VAR_DECL
w1 = SIMPLE_ID -> PRED_NAME -> VAR_DECL
mkVarDecl (String -> SIMPLE_ID
mkSimpleId "w") PRED_NAME
worldSort
w2 :: VAR_DECL
w2 :: VAR_DECL
w2 = SIMPLE_ID -> PRED_NAME -> VAR_DECL
mkVarDecl (String -> SIMPLE_ID
mkSimpleId "w'") PRED_NAME
worldSort
{- mkVarDecl doesn't support arrays as arg
mkForall doesn't support single elements as arg -}
wA :: [VAR_DECL]
wA :: [VAR_DECL]
wA = [[SIMPLE_ID] -> PRED_NAME -> Range -> VAR_DECL
Var_decl [String -> SIMPLE_ID
mkSimpleId "w", String -> SIMPLE_ID
mkSimpleId "w'"] PRED_NAME
worldSort Range
nullRange]

-- Auxiliar function 1
fromSort :: [SORT] -> [VAR_DECL]
fromSort :: [PRED_NAME] -> [VAR_DECL]
fromSort = (Int, [VAR_DECL]) -> [VAR_DECL]
forall a b. (a, b) -> b
snd ((Int, [VAR_DECL]) -> [VAR_DECL])
-> ([PRED_NAME] -> (Int, [VAR_DECL])) -> [PRED_NAME] -> [VAR_DECL]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PRED_NAME -> (Int, [VAR_DECL]) -> (Int, [VAR_DECL]))
-> (Int, [VAR_DECL]) -> [PRED_NAME] -> (Int, [VAR_DECL])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr PRED_NAME -> (Int, [VAR_DECL]) -> (Int, [VAR_DECL])
forall a.
(Num a, Show a) =>
PRED_NAME -> (a, [VAR_DECL]) -> (a, [VAR_DECL])
f (0 :: Int, [])
        where
              f :: PRED_NAME -> (a, [VAR_DECL]) -> (a, [VAR_DECL])
f so :: PRED_NAME
so (i :: a
i, xs :: [VAR_DECL]
xs) = (a
i a -> a -> a
forall a. Num a => a -> a -> a
+ 1, SIMPLE_ID -> PRED_NAME -> VAR_DECL
mkVarDecl (a -> SIMPLE_ID
forall a. Show a => a -> SIMPLE_ID
str a
i) PRED_NAME
so VAR_DECL -> [VAR_DECL] -> [VAR_DECL]
forall a. a -> [a] -> [a]
: [VAR_DECL]
xs)
              str :: a -> SIMPLE_ID
str i :: a
i = String -> SIMPLE_ID
mkSimpleId (String -> SIMPLE_ID) -> String -> SIMPLE_ID
forall a b. (a -> b) -> a -> b
$ 'x' Char -> ShowS
forall a. a -> [a] -> [a]
: a -> String
forall a. Show a => a -> String
show a
i

-- Auxiliar function 2
fromDecls :: [VAR_DECL] -> [TERM f]
fromDecls :: [VAR_DECL] -> [TERM f]
fromDecls = (VAR_DECL -> [TERM f]) -> [VAR_DECL] -> [TERM f]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap VAR_DECL -> [TERM f]
forall f. VAR_DECL -> [TERM f]
fromDecl

-- Auxiliar function 3
fromDecl :: VAR_DECL -> [TERM f]
fromDecl :: VAR_DECL -> [TERM f]
fromDecl (Var_decl vs :: [SIMPLE_ID]
vs s :: PRED_NAME
s _ ) = (SIMPLE_ID -> TERM f) -> [SIMPLE_ID] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map (SIMPLE_ID -> PRED_NAME -> TERM f
forall f. SIMPLE_ID -> PRED_NAME -> TERM f
`mkVarTerm` PRED_NAME
s) [SIMPLE_ID]
vs