ToSExpr.hs revision dece9056c18ada64bcc8f2fba285270374139ee8
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : translate VSE to S-Expressions
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiCopyright : (c) C. Maeder, DFKI 2008
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : portable
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskitranslation of VSE to S-Expressions
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangimport qualified Common.Lib.MapSet as MapSet
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederimport qualified Data.Map as Map
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederimport Data.Char (toLower)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangimport Data.Ord (comparing)
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian MaederaddUniformRestr :: Sign f Procs -> [Named Sentence] ->
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (Sign f Procs, [Named Sentence])
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederaddUniformRestr sig nsens = let
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski namedConstr = filter (\ ns -> case sentence ns of
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (RestrictedConstraint _ _ _)
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder _ -> False ) nsens
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich restrConstr = map sentence namedConstr
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich restrToSExpr (procs, tSens)
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich (Ranged (RestrictedConstraint constrs restr _flag) _r)) =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (genSorts, genOps, _maps) = recover_Sort_gen_ax constrs
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski genUniform sorts ops s = let
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder hasResSort sn ~(Qual_op_name _ opType _) = res_OP_TYPE opType == sn
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder argLength ~(Qual_op_name _ (Op_type _ args _ _) _) = length args
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder ctors = sortBy (comparing argLength) $ filter (hasResSort s) ops
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu genCodeForCtor ~(Qual_op_name ctor (Op_type _ args sn _) _) prg = let
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder decls = genVars args
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder vs = map (\ (i, a) -> Var_decl [i] a nullRange) decls
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder recCalls = map (\ (i, x) ->
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Ranged (Call (Predication
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder (Qual_pred_name
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder (gnUniformName s)
8e80792f474d154ff11762fac081a422e34f1accChristian Maeder (Pred_type [x] nullRange) nullRange)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder [Qual_var i x nullRange] nullRange
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder )) nullRange) $
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder filter (flip elem sorts . snd) decls
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder recCallsSeq = if null recCalls then Ranged Skip nullRange else
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder foldr1 (\ p1 p2 -> Ranged (Seq p1 p2) nullRange) recCalls
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder in case recCalls of
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder [] -> Ranged (
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder Block (Var_decl [yVar] s nullRange : vs)
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder (Assign yVar (Qual_var xVar sn nullRange)
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder (Ranged (Seq (Ranged
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder (Qual_op_name
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder (Op_type Partial args sn nullRange)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (map toQualVar vs)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder (Ranged (If (Strong_equation
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder (Op_type Partial [s, s]
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski uBoolean nullRange)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder aTrue nullRange)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (Ranged Skip nullRange)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder prg) nullRange))
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder nullRange )) nullRange) ) nullRange
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski _ -> Ranged (
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Block (Var_decl [yVar] s nullRange : vs)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (Ranged (Seq (Ranged (Assign yVar
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (Qual_var xVar sn nullRange)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (Seq recCallsSeq
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder (Qual_op_name
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder (Op_type Partial args sn nullRange)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (map toQualVar vs)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (Ranged (If (Strong_equation
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ( Application
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ( Qual_op_name
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (Op_type Partial [s, s]
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder uBoolean nullRange)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder aTrue nullRange)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (Ranged Skip nullRange) prg) nullRange))
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder nullRange )) nullRange)) nullRange) ) nullRange
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder [makeNamed "" $ ExtFORMULA $
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Ranged (Defprocs [
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Defproc Proc (gnUniformName s) [xVar]
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder Block [] ( foldr genCodeForCtor (Ranged Abort nullRange)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (makeNamed "" $
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Quantification Universal [Var_decl [xVar] s nullRange]
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ( ExtFORMULA $ Ranged
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (Dlformula Diamond ( Ranged
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (Call $ Predication
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (Qual_pred_name
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (Map.findWithDefault (gnRestrName s) s restr)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (Pred_type [s] nullRange) nullRange)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder [Qual_var xVar s nullRange] nullRange) nullRange)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (True_atom nullRange))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ( ExtFORMULA $ Ranged
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (Dlformula Diamond (Ranged
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (Call $ Predication
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (Qual_pred_name (gnUniformName s)
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder (Pred_type [s] nullRange) nullRange)
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder [Qual_var xVar s nullRange] nullRange) nullRange)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (True_atom nullRange))
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder nullRange) True nullRange) nullRange) {isAxiom = False}]
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder procDefs = concatMap (genUniform genSorts genOps) genSorts
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder map (\ s -> (gnUniformName s,
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Profile [Procparam In s] Nothing)) genSorts
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (Map.union procs procs', tSens ++ procDefs)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder restrToSExpr _ _ = error "should not be anything than restricted constraints"
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (newProcs, trSens) = foldl restrToSExpr (Map.empty, []) restrConstr
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski predMap = addMapSet (predMap sig) $ procsToPredMap $ Procs newProcs,
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder extendedInfo = Procs $ Map.union newProcs (procsMap $ extendedInfo sig)},
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski nameAndDisambiguate $
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder trSens ++ filter (not . flip elem namedConstr) nsens)
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedernamedSenToSExpr :: Sign f Procs -> Named Sentence -> SExpr
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskinamedSenToSExpr sig ns =
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder [ SSymbol "asentence"
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder , SSymbol $ transString $ senAttr ns
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder , SSymbol $ if isAxiom ns then "axiom" else "obligation"
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , SSymbol $ if isAxiom ns then "proved" else "open"
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , senToSExpr sig $ sentence ns ]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskisenToSExpr :: Sign f Procs -> Sentence -> SExpr
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskisenToSExpr sig s = let ns = sentenceToSExpr sig s in case s of
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ExtFORMULA (Ranged (Defprocs _) _) ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder SList [SSymbol "defprocs-sentence", ns]
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder Sort_gen_ax _ _ ->
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder SList [SSymbol "generatedness-sentence", ns]
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder _ -> SList [SSymbol "formula-sentence", ns]
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedersentenceToSExpr :: Sign f Procs -> Sentence -> SExpr
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedersentenceToSExpr sign = let sig = addSig const sign boolSig in
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder foldFormula $ sRec sig $ dlFormulaToSExpr sig
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederdlFormulaToSExpr :: Sign f Procs -> Dlformula -> SExpr
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederdlFormulaToSExpr sig = vseFormsToSExpr sig . unRanged
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedervseFormsToSExpr :: Sign f Procs -> VSEforms -> SExpr
3df765bba27034f17ba60ee9b90d7dbd3643ea9eChristian MaedervseFormsToSExpr sig vf = case vf of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Dlformula b p s ->
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder SList [SSymbol $ case b of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Diamond -> "diamond", progToSExpr sig p, sentenceToSExpr sig s]
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Defprocs ds ->
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder SList $ SSymbol "defprocs" : map (defprocToSExpr sig) ds
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder RestrictedConstraint _ _ _ ->
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder error "restricted constraints should be handled separately"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskivDeclToSExpr :: Sign f Procs -> VarDecl -> SExpr
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedervDeclToSExpr sig (VarDecl v s m _) =
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder let vd@(SList [_, w, ty]) = varDeclToSExpr (v, s) in
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder Nothing -> vd
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Just trm -> SList [ SSymbol "vardecl", w, ty
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder , foldTerm (sRec sig $ error "vDeclToSExpr") trm ]
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederprocIdToSSymbol :: Sign f Procs -> Id -> SExpr
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederprocIdToSSymbol sig n = case lookupProc n sig of
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder Nothing -> error "procIdToSSymbol"
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder Just pr -> case profileToOpType pr of
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder Just ot -> opIdToSSymbol sig n ot
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder _ -> predIdToSSymbol sig n $ profileToPredType pr
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederprogToSExpr :: Sign f Procs -> Program -> SExpr
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederprogToSExpr sig = let
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder pRec = sRec sig (error "progToSExpr")
0b6f6d3eeb7b3b36292e60f1b3da5a5ce42eef1aChristian Maeder termToSExpr = foldTerm pRec
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder formToSExpr = foldFormula pRec
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder in foldProg FoldRec
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder { foldAbort = const $ SSymbol "abort"
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder , foldSkip = const $ SSymbol "skip"
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder , foldAssign = \ _ v t ->
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder SList [SSymbol "assign", varToSSymbol v, termToSExpr t]
0b6f6d3eeb7b3b36292e60f1b3da5a5ce42eef1aChristian Maeder , foldCall = \ (Ranged _ r) f ->
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Predication (Qual_pred_name i _ _) ts _ ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder SList $ SSymbol "call" : procIdToSSymbol sig i : map termToSExpr ts
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder _ -> sfail "Call" r
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , foldReturn = \ _ t -> SList [SSymbol "return", termToSExpr t]
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , foldBlock = \ ~(Ranged (Block vs p) _) _ _ ->
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder let (vds, q) = addInits (toVarDecl vs) p
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder ps = progToSExpr sig q
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder nvs = map (vDeclToSExpr sig) vds
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder in if null nvs then ps else SList [SSymbol "vblock", SList nvs, ps]
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder , foldSeq = \ _ s1 s2 -> SList [SSymbol "seq", s1, s2]
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder , foldIf = \ _ c s1 s2 -> SList [SSymbol "if", formToSExpr c, s1, s2]
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder , foldWhile = \ _ c s -> SList [SSymbol "while", formToSExpr c, s] }
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederdefprocToSExpr :: Sign f Procs -> Defproc -> SExpr
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederdefprocToSExpr sig (Defproc k n vs p _) = SList
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder [ SSymbol $ case k of
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder Proc -> "defproc"
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder Func -> "deffuncproc"
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder , procIdToSSymbol sig n
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder , SList $ map varToSSymbol vs
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder , progToSExpr sig p ]
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederparamToSExpr :: Procparam -> SExpr
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederparamToSExpr (Procparam k s) = SList
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder [ SSymbol $ map toLower $ show k
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder , sortToSSymbol s ]
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederprocsToSExprs :: (Id -> Bool) -> Sign f Procs -> [SExpr]
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederprocsToSExprs f sig =
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder map (\ (n, pr@(Profile as _)) -> case profileToOpType pr of
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder Nothing -> SList
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder [ SSymbol "procedure"
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder , predIdToSSymbol sig n $ profileToPredType pr
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , SList $ map paramToSExpr as ]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Just ot -> SList
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder [ SSymbol "funcprocedure"
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder , opIdToSSymbol sig n ot
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder , SList $ map sortToSSymbol $ opArgs ot
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder , sortToSSymbol $ opRes ot ])
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder $ Map.toList $ Map.filterWithKey (\ i _ -> f i)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder $ procsMap $ extendedInfo sig
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedervseSignToSExpr :: Sign f Procs -> SExpr
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskivseSignToSExpr sig =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let e = extendedInfo sig in
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder SList $ SSymbol "signature" : sortSignToSExprs sig
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski : predMapToSExprs sig (diffMapSet (predMap sig) $ procsToPredMap e)
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder ++ opMapToSExprs sig (diffOpMapSet (opMap sig) $ procsToOpMap e)
578b677874296e4ba48e57b5e4b4b0270d995603Christian Maeder ++ procsToSExprs (const True) sig
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederqualVseSignToSExpr :: SIMPLE_ID -> LibId -> Sign f Procs -> SExpr
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederqualVseSignToSExpr nodeId libId sig =
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder let e = extendedInfo sig in
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder SList $ SSymbol "signature" : sortSignToSExprs sig
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (\ k _ -> isQualNameFrom nodeId libId k)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder $ sortRel sig }
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder : predMapToSExprs sig
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (MapSet.filterWithKey (\ i _ -> isQualNameFrom nodeId libId i)
4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maeder . MapSet.difference (predMap sig) $ procsToPredMap e)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder ++ opMapToSExprs sig
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder (MapSet.filterWithKey (\ i _ -> isQualNameFrom nodeId libId i)
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder . diffOpMapSet (opMap sig) $ procsToOpMap e)
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder ++ procsToSExprs (isQualNameFrom nodeId libId) sig