fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance{- |

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceModule : $Header$

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceDescription : OMDoc-to-CASL conversion

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceCopyright : (c) Ewaryst Schulz, DFKI Bremen 2009

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceLicense : GPLv2 or higher, see LICENSE.txt

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceMaintainer : ewaryst.schulz@dfki.de

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceStability : provisional

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel MancePortability : portable

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceCASL implementation of the interface functions omdocToSym, omdocToSen

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance, addOMadtToTheory, addOmdocToTheory from class Logic. The actual

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Manceinstantiation can be found in module "CASL.Logic_CASL".

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance-}

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mancemodule CASL.OMDocImport

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance ( omdocToSym

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance , omdocToSen

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance , addOMadtToTheory

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance , addOmdocToTheory

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance ) where

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Manceimport OMDoc.DataTypes

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport Common.Id

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport Common.Result

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport Common.AS_Annotation

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport qualified Common.Lib.Rel as Rel

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport CASL.AS_Basic_CASL

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport CASL.Sign

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport CASL.OMDoc

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport Control.Monad

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport qualified Data.Map as Map

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport Data.List

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance-- * Environment Interface

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mancetype Env = SigMapI Symbol

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel MancesymbolToSort :: Symbol -> SORT

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancesymbolToSort (Symbol n SortAsItemType) = n

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancesymbolToSort s = error $ "symbolToSort: Nonsort encountered: " ++ show s

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancesymbolToOp :: Symbol -> (Id, OpType)

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancesymbolToOp (Symbol n (OpAsItemType ot)) = (n, ot)

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancesymbolToOp s = error $ "symbolToOp: Nonop encountered: " ++ show s

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancesymbolToPred :: Symbol -> (Id, PredType)

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancesymbolToPred (Symbol n (PredAsItemType pt)) = (n, pt)

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancesymbolToPred s = error $ "symbolToPred: Nonpred encountered: " ++ show s

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancelookupSymbol :: Env -> OMName -> Symbol

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancelookupSymbol e omn =

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance Map.findWithDefault

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance (error $ concat [ "lookupSymbol failed for: "

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance , show omn, "\nmap: ", show $ sigMapISymbs e])

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance omn $ sigMapISymbs e

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancelookupSort :: Env -> OMName -> SORT

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancelookupSort e = symbolToSort . lookupSymbol e

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancelookupSortOMS :: String -> Env -> OMElement -> SORT

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancelookupSortOMS msg = lookupOMS lookupSort $ msg ++ "(SORT)"

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancelookupPred :: Env -> OMName -> (Id, PredType)

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancelookupPred e = symbolToPred . lookupSymbol e

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancelookupPredOMS :: String -> Env -> OMElement -> (Id, PredType)

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancelookupPredOMS msg = lookupOMS lookupPred $ msg ++ "(PRED)"

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancelookupOp :: Env -> OMName -> (Id, OpType)

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancelookupOp e = symbolToOp . lookupSymbol e

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancelookupOpOMS :: String -> Env -> OMElement -> (Id, OpType)

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancelookupOpOMS msg = lookupOMS lookupOp $ msg ++ "(Op)"

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancelookupOMS :: (Env -> OMName -> a) -> String -> Env -> OMElement -> a

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancelookupOMS f msg e oms@(OMS (cd, omn)) =

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance if cdIsEmpty cd then f e omn

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance else error $ concat [ msg, ": lookupOMS: Nonempty cd in const: "

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance , show oms]

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancelookupOMS _ msg _ ome =

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance error $ concat [msg, ": lookupOMS: Nonsymbol: ", show ome]

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancetoOpSymb :: (Id, OpType) -> OP_SYMB

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancetoOpSymb (i, t) = Qual_op_name i (toOP_TYPE t) nullRange

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancetoPredSymb :: (Id, PredType) -> PRED_SYMB

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancetoPredSymb (i, t) = Qual_pred_name i (toPRED_TYPE t) nullRange

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance-- * TOPLEVEL Interface

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance-- | A TCSymbols is transformed to a CASL symbol with given name.

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel ManceomdocToSym :: Env -> TCElement -> String -> Result Symbol

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel ManceomdocToSym e sym@(TCSymbol _ ctp srole _) n =

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance case srole of

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance Typ | ctp == const_sort -> return $ idToSortSymbol $ nameToId n

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance | otherwise -> fail $ "omdocToSym: No sorttype for " ++ show sym

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance Obj -> return $

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance case omdocToType e ctp of

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance Left ot -> idToOpSymbol (nameToId n) ot

c92573b85930868b709024284c0f13dbcaec9554Felix Gabriel Mance Right pt -> idToPredSymbol (nameToId n) pt

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance _ -> fail $ concat [ "omdocToSym: only type or object are allowed as"

c92573b85930868b709024284c0f13dbcaec9554Felix Gabriel Mance , " symbol roles, but found: ", show srole ]

c92573b85930868b709024284c0f13dbcaec9554Felix Gabriel Mance

c92573b85930868b709024284c0f13dbcaec9554Felix Gabriel ManceomdocToSym _ sym _ = fail $ concat [ "omdocToSym: only TCSymbol is allowed,"

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance , " but found: ", show sym ]

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel ManceomdocToSen :: Env -> TCElement -> String

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance -> Result (Maybe (Named (FORMULA f)))

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel ManceomdocToSen e (TCSymbol _ t sr _) n =

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance case nameDecode n of

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance Just _ ->

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance return Nothing -- don't translate encoded names here

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance Nothing ->

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance let ns = makeNamed n $ omdocToFormula e t

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance res b = return $ Just $ ns { isAxiom = b }

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance in case sr of

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance Axiom -> res True

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance Theorem -> res False

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance _ -> return Nothing

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel ManceomdocToSen _ sym _ = fail $ concat [ "omdocToSen: only TCSymbol is allowed,"

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance , " but found: ", show sym ]

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance-- | Sort generation constraints are added as named formulas.

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel ManceaddOMadtToTheory :: Env

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance -> (Sign f e, [Named (FORMULA f)]) -> [[OmdADT]]

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance -> Result (Sign f e, [Named (FORMULA f)])

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel ManceaddOMadtToTheory e (sig, nsens) adts = do

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance sgcs <- mapR (omdocToSortGenConstraint e) adts

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance return (sig, nsens ++ sgcs)

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance-- | The subsort relation is recovered from exported sentences.

e615997caa046409fc68114cd72e10a528a4bb71Felix Gabriel ManceaddOmdocToTheory :: Env -> (Sign f e, [Named (FORMULA f)]) -> [TCElement]

e615997caa046409fc68114cd72e10a528a4bb71Felix Gabriel Mance -> Result (Sign f e, [Named (FORMULA f)])

e615997caa046409fc68114cd72e10a528a4bb71Felix Gabriel ManceaddOmdocToTheory e (sig, nsens) tcs = do

e615997caa046409fc68114cd72e10a528a4bb71Felix Gabriel Mance srel <- omdocToSortRel e tcs

e615997caa046409fc68114cd72e10a528a4bb71Felix Gabriel Mance return (sig { sortRel = Rel.transClosure srel }, nsens)

e615997caa046409fc68114cd72e10a528a4bb71Felix Gabriel Mance

e615997caa046409fc68114cd72e10a528a4bb71Felix Gabriel Mance

e615997caa046409fc68114cd72e10a528a4bb71Felix Gabriel Mance-- * Algebraic Data Types

e615997caa046409fc68114cd72e10a528a4bb71Felix Gabriel Mance

e615997caa046409fc68114cd72e10a528a4bb71Felix Gabriel ManceomdocToSortGenConstraint :: Env -> [OmdADT] -> Result (Named (FORMULA f))

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel ManceomdocToSortGenConstraint e sortdefs = do

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance -- take the last type as the type of all constraints

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance let (t, cs) = mapAccumL (const $ mkConstraint e) Generated sortdefs

e615997caa046409fc68114cd72e10a528a4bb71Felix Gabriel Mance -- TODO: do we take newSort or origSort?

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance return $ toSortGenNamed (Sort_gen_ax cs $ t == Free) $ map newSort cs

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel MancemkConstraint :: Env -> OmdADT -> (ADTType, Constraint)

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel MancemkConstraint e (ADTSortDef nm t constrs) =

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance let s = lookupSort e $ mkSimpleName nm

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance l = map (mkConstructor e s) constrs

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance in (t, Constraint s l s)

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel MancemkConstraint _ _ = error "mkConstraint: Malformed ADT expression"

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel MancemkConstructor :: Env -> SORT -> OmdADT -> (OP_SYMB, [Int])

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel MancemkConstructor e s (ADTConstr nm args) =

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance let opn = nameToId $ lookupNotation e $ mkSimpleName nm

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance l = map (mkArg e) args

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance in (Qual_op_name opn (Op_type Total l s nullRange) nullRange, [0])

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance{- we have to create the name of this injection because we throw it away

e615997caa046409fc68114cd72e10a528a4bb71Felix Gabriel Manceduring the export -}

e615997caa046409fc68114cd72e10a528a4bb71Felix Gabriel MancemkConstructor e s (ADTInsort (_, omn)) =

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance let argsort = lookupSort e omn

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance opn = mkUniqueInjName argsort s

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance in (Qual_op_name opn (Op_type Total [argsort] s nullRange) nullRange, [0])

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel MancemkConstructor _ _ _ = error "mkConstructor: Malformed ADT expression"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

e615997caa046409fc68114cd72e10a528a4bb71Felix Gabriel MancemkArg :: Env -> OmdADT -> SORT

e615997caa046409fc68114cd72e10a528a4bb71Felix Gabriel MancemkArg e (ADTArg oms _) = lookupSortOMS "mkArg" e oms

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel MancemkArg _ _ = error "mkArg: Malformed ADT expression"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance-- * Subsort Relation

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceomdocToSortRel :: Env -> [TCElement] -> Result (Rel.Rel SORT)

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceomdocToSortRel e = foldM (addMaybeToSortRel e) Rel.empty

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceaddMaybeToSortRel :: Env -> Rel.Rel SORT -> TCElement -> Result (Rel.Rel SORT)

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceaddMaybeToSortRel e r (TCSymbol n (OMA [sof, oms1, oms2]) Axiom _) =

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance case nameDecode n of

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance Just ("ST", _)

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance | sof == const_subsortof ->

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance let s1 = lookupSortOMS "addMaybeToSortRel: s1" e oms1

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance s2 = lookupSortOMS "addMaybeToSortRel: s2" e oms2

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance in return $ Rel.insertKeyOrPair s1 s2 r

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance | otherwise ->

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance do

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance warning () ("Use of subsortof in a non ST Statement: " ++ n)

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance nullRange

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance return r

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance _ -> return r

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceaddMaybeToSortRel _ r _ = return r

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance-- * Types

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceomdocToType :: Env -> OMElement -> Either OpType PredType

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceomdocToType e (OMA (c : args)) =

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance let sorts = map (lookupSortOMS "omdocToType" e) args

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance opargs = init sorts

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance oprange = last sorts

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance res | c == const_predtype = Right $ PredType sorts

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance | c == const_partialfuntype = Left $ OpType Partial opargs oprange

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance | c == const_funtype = Left $ OpType Total opargs oprange

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance | otherwise = error $ "omdocToType: unknown type constructor: "

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance ++ show c

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance in res

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceomdocToType e oms@(OMS _)

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance | oms == const_predtype = Right $ PredType []

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance | otherwise = Left $ OpType Total [] $ lookupSortOMS "omdocToType" e oms

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceomdocToType _ ome = error $ "omdocToType: Non-supported element: " ++ show ome

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance-- * Terms and Formulas

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mancetype VarMap = Map.Map VAR SORT

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mancetype TermEnv = (Env, VarMap)

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel MancemkConjunction, mkDisjunction, mkImplication, mkImplied, mkEquivalence

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance , mkNegation :: [FORMULA f] -> FORMULA f

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel MancemkConjunction l = Conjunction l nullRange

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel MancemkDisjunction l = Disjunction l nullRange

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel MancemkImplication [x, y] = Implication x y True nullRange

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel MancemkImplication _ = error "Malformed implication"

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel MancemkImplied [x, y] = Implication x y False nullRange

mkImplied _ = error "Malformed if"

mkEquivalence [x, y] = Equivalence x y nullRange

mkEquivalence _ = error "Malformed equivalence"

mkNegation [x] = Negation x nullRange

mkNegation _ = error "Malformed negation"

mkDefinedness, mkExistl_equation, mkStrong_equation

:: [TERM f] -> FORMULA f

mkDefinedness [x] = Definedness x nullRange

mkDefinedness _ = error "Malformed definedness"

mkExistl_equation [x, y] = Existl_equation x y nullRange

mkExistl_equation _ = error "Malformed existl equation"

mkStrong_equation [x, y] = Strong_equation x y nullRange

mkStrong_equation _ = error "Malformed strong equation"

-- Quantification, Predication and Membership are handled inside omdocToFormula

-- Term construction functions

mkT2 :: (OMElement -> a) -> (OMElement -> b) -> (a -> b -> Range -> TERM f)

-> [OMElement] -> TERM f

mkT2 f g c l = case l of

[x, y] -> c (f x) (g y) nullRange

_ -> error "mkT2: 2 arguments expected"

mkT3 :: (OMElement -> a) -> (OMElement -> b) -> (OMElement -> c)

-> (a -> b -> c -> Range -> TERM f) -> [OMElement] -> TERM f

mkT3 f g h c l = case l of

[x, y, z] -> c (f x) (g y) (h z) nullRange

_ -> error "mkT3: 3 arguments expected"

-- Formula construction functions

mkFF :: TermEnv -> ([FORMULA f] -> FORMULA f) -> [OMElement] -> FORMULA f

mkFF e f l = f $ map (omdocToFormula' e) l

mkTF :: TermEnv -> ([TERM f] -> FORMULA f) -> [OMElement] -> FORMULA f

mkTF e f l = f $ map (omdocToTerm' e) l

getQuantifier :: OMElement -> QUANTIFIER

getQuantifier oms

| oms == const_forall = Universal

| oms == const_exists = Existential

| oms == const_existsunique = Unique_existential

| otherwise = error $ "getQuantifier: unrecognized quantifier " ++ show oms

mkBinder :: TermEnv -> QUANTIFIER -> [OMElement] -> OMElement -> FORMULA f

mkBinder te@(e, _) q vars body =

let (vm', vardecls) = toVarDecls te vars

bd = omdocToFormula' (e, vm') body

in Quantification q vardecls bd nullRange

toVarDecls :: TermEnv -> [OMElement] -> (VarMap, [VAR_DECL])

toVarDecls (e, vm) l =

let f acc x = let (v, s) = toVarDecl e x

acc' = Map.insert v s acc

in (acc', (v, s))

(vm', l') = mapAccumL f vm l

-- group by same sort

l'' = groupBy (\ x y -> snd x == snd y) l'

-- the lists returned by groupBy are never empty, so head will succeed

g vsl = Var_decl (map fst vsl) (snd $ head vsl) nullRange

in (vm', map g l'')

-- in CASL we expect all bound vars to be attributed (typed)

toVarDecl :: Env -> OMElement -> (VAR, SORT)

toVarDecl e (OMATTT (OMV v) (OMAttr ct t))

| ct == const_type = (nameToToken $ name v, lookupSortOMS "toVarDecl" e t)

| otherwise = error $ "toVarDecl: unrecognized attribution " ++ show ct

toVarDecl _ _ = error "toVarDecl: bound variables should be attributed."

-- Toplevel entry point

omdocToFormula :: Env -> OMElement -> FORMULA f

omdocToFormula e = omdocToFormula' (e, Map.empty)

-- Functions with given VarMap

-- omdocToTerm has no toplevel entry point

omdocToTerm' :: TermEnv -> OMElement -> TERM f

omdocToTerm' e@(ie, vm) f =

case f of

OMA (h : args)

| h == const_cast ->

mkT2 (omdocToTerm' e) (lookupSortOMS "omdocToTerm: Cast" ie)

Cast args

| h == const_if ->

mkT3 (omdocToTerm' e) (omdocToFormula' e) (omdocToTerm' e)

Conditional args

-- all other heads mean application

| otherwise ->

let os = toOpSymb $ lookupOpOMS "omdocToTerm" ie h

args' = map (omdocToTerm' e) args

in Application os args' nullRange

OMS _ -> let os = toOpSymb $ lookupOpOMS "omdocToTerm-OMS:" ie f

in Application os [] nullRange

OMV omn -> let var = nameToToken $ name omn

-- lookup the type of the variable in the varmap

s = Map.findWithDefault

(error $ concat [ "omdocToTerm': Variable not in "

, "varmap: ", show var ]) var vm

in Qual_var var s nullRange

OMATTT ome (OMAttr ct t)

| ct == const_type ->

-- same as cast

mkT2 (omdocToTerm' e) (lookupSortOMS "omdocToTerm: Sorted" ie)

Sorted_term [ome, t]

| otherwise -> error $ "omdocToTerm: unrecognized attribution "

++ show ct

_ -> error $ "omdocToTerm: no valid term " ++ show f

omdocToFormula' :: TermEnv -> OMElement -> FORMULA f

omdocToFormula' e@(ie, _) f =

case f of

OMA (h : args)

| h == const_in ->

case args of

[x, s] ->

Membership (omdocToTerm' e x) (lookupSortOMS

"omdocToFormula"

ie s) nullRange

_ -> error "Malformed membership"

| h == const_and ->

mkFF e mkConjunction args

| h == const_or ->

mkFF e mkDisjunction args

| h == const_implies ->

mkFF e mkImplication args

| h == const_implied ->

mkFF e mkImplied args

| h == const_equivalent ->

mkFF e mkEquivalence args

| h == const_not ->

mkFF e mkNegation args

| h == const_def ->

mkTF e mkDefinedness args

| h == const_eeq ->

mkTF e mkExistl_equation args

| h == const_eq ->

mkTF e mkStrong_equation args

-- all other heads mean predication

| otherwise ->

let ps = toPredSymb $ lookupPredOMS "omdocToFormula" ie h

g l = Predication ps l nullRange in

mkTF e g args

OMBIND binder args body ->

mkBinder e (getQuantifier binder) args body

OMS _ | f == const_true -> True_atom nullRange

| f == const_false -> False_atom nullRange

-- Propositional Constants (0-ary predicates):

| otherwise ->

Predication (toPredSymb

$ lookupPredOMS

("omdocToFormula: can't handle constant "

++ show f) ie f) [] nullRange

_ -> error $ "omdocToFormula: no valid formula " ++ show f