{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

{- |

Module : $Header$

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 Show

-- Just to make things easier to understand

type HForm = HybridFORMULA

type CForm = CASLFORMULA

type CSign = CASLSign

instance Language Hybrid2CASL where

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

sourceSublogic Hybrid2CASL = ()

targetLogic Hybrid2CASL = CASL

mapSublogic Hybrid2CASL _ = Just SL.caslTop

{ SL.cons_features = SL.emptyMapConsFeature

, SL.sub_features = SL.NoSub

}

map_theory Hybrid2CASL = transTheory

has_model_expansion Hybrid2CASL = True

is_weakly_amalgamable Hybrid2CASL = True

is_model_transportable Hybrid2CASL = True

isInclusionComorphism Hybrid2CASL = 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 (s, fs) = let

newSig = transSig s

fs' = fmap (mapNamed trans) fs

fs'' = dataTrans (fs ++ sentences s)

newSens = fs' ++ sentences newSig ++ fs''

rigidP = applRig (rigidPreds $ extendedInfo s) "RigidPred" gnPCons

rigidO = applRig (rigidOps $ extendedInfo s) "RigidOp" gnOCons

in return (newSig, rigidP ++ rigidO ++ newSens)

-- Special formulas not covered by normal hybridization

dataTrans :: [Named HForm] -> [Named CForm]

dataTrans = foldr f []

where

f a b = case sentence a of

Sort_gen_ax a' b' -> a { sentence = Sort_gen_ax a' b' } : b

_ -> b

transSig :: HSign -> CSign

transSig hs = let

workflow = transSens hs . addWrldArg hs

workflow' = addRels hs . addWorlds hs

in workflow . workflow' $ newSign hs

{- Creates a new CASL signature based on the hybrid Sig

Also adds the world sort. -}

newSign :: HSign -> CSign

newSign hs = (emptySign ())

{ sortRel = Rel.insertKey worldSort $ sortRel hs

, emptySortSet = emptySortSet hs

, assocOps = assocOps hs

, varMap = varMap hs

, declaredSymbols = declaredSymbols hs

, envDiags = envDiags hs

, annoMap = annoMap hs

, globAnnos = globAnnos hs

, opMap = addOpMapSet (rigidOps $ extendedInfo hs) (opMap hs)

, predMap = addMapSet (rigidPreds $ extendedInfo hs) (predMap hs)

}

{- | Adds the World constants, based

on the nominals in HSign -}

addWorlds :: HSign -> CSign -> CSign

addWorlds hs cs =

let getWorld = OpType Total [] worldSort

s = extendedInfo hs

kl = Map.keys $ nomies s

workflow = stringToId . ("Wrl_" ++) . tokStr

il = fmap workflow kl

ins = foldr (\ k m -> MapSet.insert k getWorld m) (opMap cs) il

in cs { opMap = ins }

{- | Adds the Accessibility relation, based

ono the modalities found in HSign -}

addRels :: HSign -> CSign -> CSign

addRels hs cs =

let accRelT = PredType [worldSort, worldSort]

s = extendedInfo hs

kl = Map.keys $ modies s

il = fmap (stringToId . ("Acc_" ++) . tokStr) kl

ins = foldl (\ m k -> MapSet.insert k accRelT m) (predMap cs) il

in cs { predMap = 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 hs cs = let

f (OpType a b c) = OpType a (worldSort : b) c

g (PredType a) = PredType (worldSort : a)

ops = addOpMapSet (rigidOps $ extendedInfo hs) (opMap hs)

preds = addMapSet (rigidPreds $ extendedInfo hs) (predMap hs)

ks = Set.elems $ MapSet.keysSet ops

ks' = Set.elems $ MapSet.keysSet preds

in cs

{ opMap = foldr (MapSet.update (Set.map f)) (opMap cs) ks

, predMap = foldr (MapSet.update (Set.map g)) (predMap cs) 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 hs cs = let

mods = Map.elems (modies $ extendedInfo hs)

noms = Map.elems (nomies $ extendedInfo hs)

fs = concat $ mods ++ noms

workflow = makeNamed "" . trans . item

fs' = fmap workflow fs

fs'' = fmap (mapNamed trans) (sentences hs)

in cs { sentences = fs' ++ fs'' }

-- Translates an HybridCASL formula to CASL formula

trans :: HForm -> CForm

trans = let w = mkSimpleId "world"

vars = mkVarDecl w worldSort

in mkForall [vars] . trForm (QtM w) []

{- | Formula translator

The 2nd argument is used to store the reserved words -}

trForm :: Mode -> [String] -> HForm -> CForm

trForm w s b = case b of

ExtFORMULA f -> alpha w s f

Junction j fs r -> Junction j (fmap (trForm w s) fs) r

Relation f r f' q -> Relation (trForm w s f) r (trForm w s f') q

Negation f _ -> mkNeg $ trForm w s f

Predication p l _ -> mkPredication (mkPName p) $ trTerms w s l

Quantification q l f r -> Quantification q l (trForm w s f) r

Definedness t _ -> Definedness (trTerm w s t) nullRange

Atom a r -> Atom a r

_ -> error "Hybrid2CASL.trForm"

-- | Alpha function, translates pure Hybrid Formulas

alpha :: Mode -> [String] -> H_FORMULA -> CForm

alpha w s b = case b of

Here n _ -> mkStEq (mkArg (Right n) s) $ case w of

QtM wm -> mkVarTerm wm worldSort

_ -> mkArg (Left w) s

BoxOrDiamond True m f _ -> trBox w m s f

BoxOrDiamond False m f _ -> trForm w s $ toBox m f

At (Simple_nom n) f _ -> trForm (AtM n) s f

Univ n f _ -> trForall w n s f

Exist n f _ -> mkNeg $ trForall w n s (mkNeg f)

where

toBox m f = mkNeg . ExtFORMULA $ BoxOrDiamond True m (mkNeg f) nullRange

-- | Function that takes care of formulas of box type

trBox :: Mode -> MODALITY -> [String] -> HForm -> CForm

trBox m (Simple_mod m') s f = quant $ mkImpl prd $ trForm (QtM v) ss f

where

quant = mkForall [var]

var = mkVarDecl v worldSort

v = mkSimpleId $ head ss

ss = newVarName s

prd = mkPredication predN $ predA m

predN = qp m' t

predA w = [mkArg (Left w) s, mkArg (Left (QtM v)) s]

qp x = mkQualPred (stringToId . ("Acc_" ++) $ show x)

t = Pred_type [worldSort, worldSort] nullRange

trBox _ _ _ _ = trueForm

-- translation function for the quantification of nominals case

trForall :: Mode -> NOMINAL -> [String] -> HForm -> CForm

trForall w (Simple_nom a) s f = mkForall [mkVarDecl a worldSort]

$ trForm w (show a : s) f

-- Function that translates a list of hybrid terms to casl terms

trTerms :: Mode -> [String] -> [TERM H_FORMULA] -> [TERM ()]

trTerms m s l = mkArg (Left m) s : fmap (trTerm m s) l

-- Function that translates hybrid term to casl term

trTerm :: Mode -> [String] -> TERM H_FORMULA -> TERM ()

trTerm m s t = case t of

Qual_var v s' x -> Qual_var v s' x

Application o l r -> Application (mkOName o) (trTerms m s l) r

Sorted_term t' s' r -> Sorted_term (trTerm m s t') s' r

_ -> error "Hybrid2CASL.trTerm"

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

-- The world sort type

worldSort :: SORT

worldSort = stringToId "World"

mkPName :: PRED_SYMB -> PRED_SYMB

mkPName ~(Qual_pred_name n t _) = mkQualPred n (f t)

where f (Pred_type l r) = Pred_type (worldSort : l) r

mkOName :: OP_SYMB -> OP_SYMB

mkOName ~(Qual_op_name n t _) = mkQualOp n (f t)

where f (Op_type o l s r) = Op_type o (worldSort : l) s 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 a l = case a of

Left (QtM w) -> vt w

Left (AtM w) -> ch tokStr w

Right (Simple_nom n) -> ch show n

where

vt x = mkVarTerm x worldSort

ap x = mkAppl (qo x t) []

ch f x = if f x `elem` l then vt x else ap x

qo x = mkQualOp $ stringToId . ("Wrl_" ++) $ show x

t = Op_type Total [] worldSort nullRange

-- Create a new variable name new in the formula

newVarName :: [String] -> [String]

newVarName xs = ("world" ++) (show $ length xs) : 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 s = fmap $ makeNamed 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 m s f = toName s $ glueDs ks f m

where ks = Set.elems $ MapSet.keysSet 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 ks f m = concat $ foldr (\ a b -> g a : b) [] ks

where g k = glueDe k (MapSet.lookup k m) 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 n s f = foldr (\ a b -> f n a : b) [] $ Set.elems 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 n (PredType ts) = mkForall decls $ mkForall wA $ mkImpl f1 f2

where f1 = mkPredication predName $ terms w1

f2 = mkPredication predName $ terms w2

decls = fromSort ts

terms x = fromDecls $ x : decls

predName = mkQualPred n $ mkPredType ts

mkPredType x = Pred_type (worldSort : x) nullRange

gnOCons :: OP_NAME -> OpType -> CForm

gnOCons n (OpType o ts t) = mkForall decls $ mkForall wA f

where f = mkStEq (mkAppl opName $ terms w1) t2

t2 = mkAppl opName $ terms w2

decls = fromSort ts

terms x = fromDecls $ x : decls

opName = mkQualOp n $ mkOpType o (worldSort : ts) t

mkOpType x y z = Op_type x y z 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 = mkVarDecl (mkSimpleId "w") worldSort

w2 :: VAR_DECL

w2 = mkVarDecl (mkSimpleId "w'") worldSort

{- mkVarDecl doesn't support arrays as arg

mkForall doesn't support single elements as arg -}

wA :: [VAR_DECL]

wA = [Var_decl [mkSimpleId "w", mkSimpleId "w'"] worldSort nullRange]

-- Auxiliar function 1

fromSort :: [SORT] -> [VAR_DECL]

fromSort = snd . foldr f (0 :: Int, [])

where

f so (i, xs) = (i + 1, mkVarDecl (str i) so : xs)

str i = mkSimpleId $ 'x' : show i

-- Auxiliar function 2

fromDecls :: [VAR_DECL] -> [TERM f]

fromDecls = concatMap fromDecl

-- Auxiliar function 3

fromDecl :: VAR_DECL -> [TERM f]

fromDecl (Var_decl vs s _ ) = map (`mkVarTerm` s) vs