81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
db9680b2bbd9d091b198eaa4e324762921965fb3Christian MaederCopyright : nevrenato@gmail.com
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederLicense : GPLv2 or higher, see LICENSE.txt
db9680b2bbd9d091b198eaa4e324762921965fb3Christian MaederMaintainer : Christian.Maeder@dfki.de
db9680b2bbd9d091b198eaa4e324762921965fb3Christian MaederStability : experimental
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederPortability : non-portable (imports Logic.Logic)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederComorphism HybridCASL to CASL.
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder ( Hybrid2CASL (..)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederimport qualified Common.Lib.Rel as Rel
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maederimport qualified Common.Lib.MapSet as MapSet
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederimport qualified Data.Set as Set
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maederimport qualified Data.Map as Map
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederdata Hybrid2CASL = Hybrid2CASL deriving Show
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder-- Just to make things easier to understand
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroedertype HForm = HybridFORMULA
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroedertype CForm = CASLFORMULA
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroedertype CSign = CASLSign
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederinstance Language Hybrid2CASL where
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder language_name Hybrid2CASL = "Hybrid2CASL"
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederinstance Comorphism Hybrid2CASL
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder H_BASIC_SPEC HForm SYMB_ITEMS SYMB_MAP_ITEMS
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder Symbol RawSymbol ()
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder CASLBasicSpec CForm SYMB_ITEMS SYMB_MAP_ITEMS
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Symbol RawSymbol ProofTree where
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder sourceLogic Hybrid2CASL = Hybrid
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder sourceSublogic Hybrid2CASL = ()
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder targetLogic Hybrid2CASL = CASL
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder mapSublogic Hybrid2CASL _ = Just SL.caslTop
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder { SL.cons_features = SL.emptyMapConsFeature
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder map_theory Hybrid2CASL = transTheory
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder has_model_expansion Hybrid2CASL = True
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder is_weakly_amalgamable Hybrid2CASL = True
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder is_model_transportable Hybrid2CASL = True
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder isInclusionComorphism Hybrid2CASL = True
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder{- Translates the given theory in an HybridCASL form to an equivalent
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maedertheory in CASL form
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian MaederQuestion : Why some sentences are in the sig and other sentences are
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maederin the 2nd argument ? (this is scary)
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maederfs'' is needed for special sentences, refering about datatypes
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maederfor which hybridization has nothing to do -}
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedertransTheory :: (HSign, [Named HForm]) -> Result (CSign, [Named CForm])
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian MaedertransTheory (s, fs) = let
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder newSig = transSig s
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder fs' = fmap (mapNamed trans) fs
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder fs'' = dataTrans (fs ++ sentences s)
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder newSens = fs' ++ sentences newSig ++ fs''
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder rigidP = applRig (rigidPreds $ extendedInfo s) "RigidPred" gnPCons
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder rigidO = applRig (rigidOps $ extendedInfo s) "RigidOp" gnOCons
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder in return (newSig, rigidP ++ rigidO ++ newSens)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder-- Special formulas not covered by normal hybridization
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederdataTrans :: [Named HForm] -> [Named CForm]
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederdataTrans = foldr f []
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder f a b = case sentence a of
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder Sort_gen_ax a' b' -> a { sentence = Sort_gen_ax a' b' } : b
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedertransSig :: HSign -> CSign
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian MaedertransSig hs = let
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder workflow = transSens hs . addWrldArg hs
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder workflow' = addRels hs . addWorlds hs
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder in workflow . workflow' $ newSign hs
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder{- Creates a new CASL signature based on the hybrid Sig
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian MaederAlso adds the world sort. -}
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedernewSign :: HSign -> CSign
db9680b2bbd9d091b198eaa4e324762921965fb3Christian MaedernewSign hs = (emptySign ())
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder { sortRel = Rel.insertKey worldSort $ sortRel hs
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder , emptySortSet = emptySortSet hs
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder , assocOps = assocOps hs
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder , varMap = varMap hs
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder , declaredSymbols = declaredSymbols hs
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder , envDiags = envDiags hs
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder , annoMap = annoMap hs
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder , globAnnos = globAnnos hs
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder , opMap = addOpMapSet (rigidOps $ extendedInfo hs) (opMap hs)
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder , predMap = addMapSet (rigidPreds $ extendedInfo hs) (predMap hs)
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder{- | Adds the World constants, based
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maederon the nominals in HSign -}
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederaddWorlds :: HSign -> CSign -> CSign
db9680b2bbd9d091b198eaa4e324762921965fb3Christian MaederaddWorlds hs cs =
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder let getWorld = OpType Total [] worldSort
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder s = extendedInfo hs
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder kl = Map.keys $ nomies s
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder workflow = stringToId . ("Wrl_" ++) . tokStr
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder il = fmap workflow kl
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder ins = foldr (\ k m -> MapSet.insert k getWorld m) (opMap cs) il
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder in cs { opMap = ins }
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder{- | Adds the Accessibility relation, based
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maederono the modalities found in HSign -}
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederaddRels :: HSign -> CSign -> CSign
db9680b2bbd9d091b198eaa4e324762921965fb3Christian MaederaddRels hs cs =
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder let accRelT = PredType [worldSort, worldSort]
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder s = extendedInfo hs
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder kl = Map.keys $ modies s
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder il = fmap (stringToId . ("Acc_" ++) . tokStr) kl
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder ins = foldl (\ m k -> MapSet.insert k accRelT m) (predMap cs) il
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder in cs { predMap = ins }
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder{- | Adds one argument of type World to all preds and ops
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maederdefinitions in an hybrid signature and passes them to a caslsig -}
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederaddWrldArg :: HSign -> CSign -> CSign
db9680b2bbd9d091b198eaa4e324762921965fb3Christian MaederaddWrldArg hs cs = let
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder f (OpType a b c) = OpType a (worldSort : b) c
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder g (PredType a) = PredType (worldSort : a)
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder ops = addOpMapSet (rigidOps $ extendedInfo hs) (opMap hs)
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder preds = addMapSet (rigidPreds $ extendedInfo hs) (predMap hs)
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder { opMap = foldr (MapSet.update (Set.map f)) (opMap cs) ks
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder , predMap = foldr (MapSet.update (Set.map g)) (predMap cs) ks'
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder{- Translates all hybridformulas in a hybridSig to caslformulas
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian MaederOnes are in the declaration of nominals and modalities (however
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maederfor nows that is forbidden to happen)
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian MaederThe others come from the casl sig -}
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedertransSens :: HSign -> CSign -> CSign
db9680b2bbd9d091b198eaa4e324762921965fb3Christian MaedertransSens hs cs = let
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder mods = Map.elems (modies $ extendedInfo hs)
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder noms = Map.elems (nomies $ extendedInfo hs)
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder fs = concat $ mods ++ noms
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder workflow = makeNamed "" . trans . item
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder fs' = fmap workflow fs
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder fs'' = fmap (mapNamed trans) (sentences hs)
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder in cs { sentences = fs' ++ fs'' }
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder-- Translates an HybridCASL formula to CASL formula
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroedertrans :: HForm -> CForm
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroedertrans = let w = mkSimpleId "world"
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder vars = mkVarDecl w worldSort
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder in mkForall [vars] . trForm (QtM w) []
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder{- | Formula translator
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian MaederThe 2nd argument is used to store the reserved words -}
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedertrForm :: Mode -> [String] -> HForm -> CForm
db9680b2bbd9d091b198eaa4e324762921965fb3Christian MaedertrForm w s b = case b of
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder ExtFORMULA f -> alpha w s f
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder Junction j fs r -> Junction j (fmap (trForm w s) fs) r
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder Relation f r f' q -> Relation (trForm w s f) r (trForm w s f') q
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder Negation f _ -> mkNeg $ trForm w s f
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder Predication p l _ -> mkPredication (mkPName p) $ trTerms w s l
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder Quantification q l f r -> Quantification q l (trForm w s f) r
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder Definedness t _ -> Definedness (trTerm w s t) nullRange
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder Atom a r -> Atom a r
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder-- | Alpha function, translates pure Hybrid Formulas
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederalpha :: Mode -> [String] -> H_FORMULA -> CForm
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maederalpha w s b = case b of
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder Here n _ -> mkStEq (mkArg (Right n) s) $ case w of
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder QtM wm -> mkVarTerm wm worldSort
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder _ -> mkArg (Left w) s
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder BoxOrDiamond True m f _ -> trBox w m s f
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder BoxOrDiamond False m f _ -> trForm w s $ toBox m f
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder At (Simple_nom n) f _ -> trForm (AtM n) s f
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder Univ n f _ -> trForall w n s f
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder Exist n f _ -> mkNeg $ trForall w n s (mkNeg f)
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder toBox m f = mkNeg . ExtFORMULA $ BoxOrDiamond True m (mkNeg f) nullRange
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder-- | Function that takes care of formulas of box type
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedertrBox :: Mode -> MODALITY -> [String] -> HForm -> CForm
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedertrBox m (Simple_mod m') s f = quant $ mkImpl prd $ trForm (QtM v) ss f
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder quant = mkForall [var]
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder var = mkVarDecl v worldSort
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder v = mkSimpleId $ head ss
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder ss = newVarName s
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder prd = mkPredication predN $ predA m
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder predN = qp m' t
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder predA w = [mkArg (Left w) s, mkArg (Left (QtM v)) s]
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder qp x = mkQualPred (stringToId . ("Acc_" ++) $ show x)
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder t = Pred_type [worldSort, worldSort] nullRange
db9680b2bbd9d091b198eaa4e324762921965fb3Christian MaedertrBox _ _ _ _ = trueForm
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder-- translation function for the quantification of nominals case
db9680b2bbd9d091b198eaa4e324762921965fb3Christian MaedertrForall :: Mode -> NOMINAL -> [String] -> HForm -> CForm
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian MaedertrForall w (Simple_nom a) s f = mkForall [mkVarDecl a worldSort]
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder $ trForm w (show a : s) f
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder-- Function that translates a list of hybrid terms to casl terms
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedertrTerms :: Mode -> [String] -> [TERM H_FORMULA] -> [TERM ()]
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedertrTerms m s l = mkArg (Left m) s : fmap (trTerm m s) l
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder-- Function that translates hybrid term to casl term
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian MaedertrTerm :: Mode -> [String] -> TERM H_FORMULA -> TERM ()
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedertrTerm m s t = case t of
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder Qual_var v s' x -> Qual_var v s' x
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder Application o l r -> Application (mkOName o) (trTerms m s l) r
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder Sorted_term t' s' r -> Sorted_term (trTerm m s t') s' r
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder-- **** Auxiliar functions and datatype ****
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder-- The world sort type
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederworldSort :: SORT
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederworldSort = stringToId "World"
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedermkPName :: PRED_SYMB -> PRED_SYMB
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedermkPName ~(Qual_pred_name n t _) = mkQualPred n (f t)
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder where f (Pred_type l r) = Pred_type (worldSort : l) r
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedermkOName :: OP_SYMB -> OP_SYMB
db9680b2bbd9d091b198eaa4e324762921965fb3Christian MaedermkOName ~(Qual_op_name n t _) = mkQualOp n (f t)
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder where f (Op_type o l s r) = Op_type o (worldSort : l) s r
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder{- Function that will decide how to create a new argument
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian MaederThat argument can be a variable or a nominal (constant) -}
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian MaedermkArg :: Either Mode NOMINAL -> [String] -> TERM ()
db9680b2bbd9d091b198eaa4e324762921965fb3Christian MaedermkArg a l = case a of
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Left (QtM w) -> vt w
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Left (AtM w) -> ch tokStr w
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Right (Simple_nom n) -> ch show n
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder vt x = mkVarTerm x worldSort
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder ap x = mkAppl (qo x t) []
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder ch f x = if f x `elem` l then vt x else ap x
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder qo x = mkQualOp $ stringToId . ("Wrl_" ++) $ show x
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder t = Op_type Total [] worldSort nullRange
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder-- Create a new variable name new in the formula
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedernewVarName :: [String] -> [String]
db9680b2bbd9d091b198eaa4e324762921965fb3Christian MaedernewVarName xs = ("world" ++) (show $ length xs) : xs
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder{- | Auxiliar datatype to determine wich is the argument of alpha
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian MaederQuantified Mode or At mode -}
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederdata Mode = QtM VAR | AtM SIMPLE_ID
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder-- **** End of auxiliar functions and datatypes section ****************
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder-- ----- Generation of constraints associated with rigid designators
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedertoName :: (Functor f) => String -> f a -> f (Named a)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedertoName s = fmap $ makeNamed s
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder{- Adds the constraints associated with the rigidity
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maederof predicates or operations. -}
db9680b2bbd9d091b198eaa4e324762921965fb3Christian MaederapplRig :: (Ord k) => MapSet.MapSet k a ->
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder (k -> a -> CForm) ->
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederapplRig m s f = toName s $ glueDs ks f m
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder{- Given a list of designators, generates the rigidity constraints
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maederassociated, and concats them into a single list -}
db9680b2bbd9d091b198eaa4e324762921965fb3Christian MaederglueDs :: (Ord k) => [k] ->
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder (k -> a -> CForm) ->
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian MaederglueDs ks f m = concat $ foldr (\ a b -> g a : b) [] ks
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder where g k = glueDe k (MapSet.lookup k m) f
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder{- Given a single designator, genereates the rigidity constraints
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maederassociated, and joins them into a single list -}
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederglueDe :: k -> Set.Set a -> (k -> a -> CForm) -> [CForm]
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian MaederglueDe n s f = foldr (\ a b -> f n a : b) [] $ Set.elems s
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder{- Generates a rigid constraint from a single pred name and type
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian MaederWe add the extra world argument in mkPredType so that it coincides
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maederwith the later translated predicate definition -}
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedergnPCons :: PRED_NAME -> PredType -> CForm
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedergnPCons n (PredType ts) = mkForall decls $ mkForall wA $ mkImpl f1 f2
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder where f1 = mkPredication predName $ terms w1
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder f2 = mkPredication predName $ terms w2
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder decls = fromSort ts
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder terms x = fromDecls $ x : decls
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder predName = mkQualPred n $ mkPredType ts
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder mkPredType x = Pred_type (worldSort : x) nullRange
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedergnOCons :: OP_NAME -> OpType -> CForm
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian MaedergnOCons n (OpType o ts t) = mkForall decls $ mkForall wA f
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder where f = mkStEq (mkAppl opName $ terms w1) t2
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder t2 = mkAppl opName $ terms w2
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder decls = fromSort ts
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder terms x = fromDecls $ x : decls
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder opName = mkQualOp n $ mkOpType o (worldSort : ts) t
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder mkOpType x y z = Op_type x y z nullRange
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder{- The next functions are auxiliar. They are need for generating the
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maederproper variables/terms for the quantifiers,predications and operations. -}
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederw1 = mkVarDecl (mkSimpleId "w") worldSort
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederw2 = mkVarDecl (mkSimpleId "w'") worldSort
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder{- mkVarDecl doesn't support arrays as arg
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian MaedermkForall doesn't support single elements as arg -}
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederwA :: [VAR_DECL]
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian MaederwA = [Var_decl [mkSimpleId "w", mkSimpleId "w'"] worldSort nullRange]
db9680b2bbd9d091b198eaa4e324762921965fb3Christian Maeder-- Auxiliar function 1
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederfromSort :: [SORT] -> [VAR_DECL]
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian MaederfromSort = snd . foldr f (0 :: Int, [])
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder f so (i, xs) = (i + 1, mkVarDecl (str i) so : xs)
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian Maeder str i = mkSimpleId $ 'x' : show i
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder-- Auxiliar function 2
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederfromDecls :: [VAR_DECL] -> [TERM f]
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian MaederfromDecls = concatMap fromDecl
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder-- Auxiliar function 3
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederfromDecl :: VAR_DECL -> [TERM f]
7a7d13f347477e6daa89b9322aed2985dd7f9c56Christian MaederfromDecl (Var_decl vs s _ ) = map (`mkVarTerm` s) vs