a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederDescription : translate CASL to S-Expressions
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederCopyright : (c) C. Maeder, DFKI 2008
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederMaintainer : Christian.Maeder@dfki.de
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederStability : provisional
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederPortability : portable
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maedertranslation of CASL to S-Expressions
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Common.Lib.MapSet as MapSet
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maederimport qualified Data.Map as Map
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maederimport qualified Data.Set as Set
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maederimport qualified Data.List as List
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaederpredToSSymbol :: Sign f e -> PRED_SYMB -> SExpr
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaederpredToSSymbol sign p = case p of
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder Pred_name _ -> error "predToSSymbol"
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder Qual_pred_name i t _ -> predIdToSSymbol sign i $ toPredType t
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian MaederpredIdToSSymbol :: Sign f e -> Id -> PredType -> SExpr
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederpredIdToSSymbol sign i t =
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder case List.elemIndex t . Set.toList . MapSet.lookup i $ predMap sign of
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder Nothing -> error "predIdToSSymbol"
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder Just n -> idToSSymbol (n + 1) i
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaederopToSSymbol :: Sign f e -> OP_SYMB -> SExpr
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian MaederopToSSymbol sign o = case o of
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder Op_name _ -> error "opToSSymbol"
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder Qual_op_name i t _ -> opIdToSSymbol sign i $ toOpType t
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian MaederopIdToSSymbol :: Sign f e -> Id -> OpType -> SExpr
4e14c1bc2b97679b84c6ad996fa11c273b74ea02Christian MaederopIdToSSymbol sign i t = case List.findIndex
4e14c1bc2b97679b84c6ad996fa11c273b74ea02Christian Maeder (on (==) opSorts t) . Set.toList
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder . MapSet.lookup i $ opMap sign of
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder Nothing -> error $ "opIdToSSymbol " ++ show i
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder Just n -> idToSSymbol (n + 1) i
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian MaedersortToSSymbol :: Id -> SExpr
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian MaedersortToSSymbol = idToSSymbol 0
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaedervarToSSymbol :: Token -> SExpr
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaedervarToSSymbol = SSymbol . transToken
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaedervarDeclToSExpr :: (VAR, SORT) -> SExpr
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaedervarDeclToSExpr (v, s) =
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder SList [SSymbol "vardecl-indet", varToSSymbol v, sortToSSymbol s]
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maedersfail :: String -> Range -> a
05b9abe2e7d9e6126bf4ae29be6ef3693f32de73Christian Maedersfail s = error . show . Diag Error ("unexpected " ++ s)
ca0d4947f7b0fdcbf7eac627659e6cff6d3863baChristian MaedersRec :: GetRange f => Sign a e -> (f -> SExpr) -> Record f SExpr SExpr
bb2c1beb7ab66a49627a2a34df80864a3c65cc83Christian MaedersRec sign mf = Record
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder { foldQuantification = \ _ q vs f _ ->
bb2c1beb7ab66a49627a2a34df80864a3c65cc83Christian Maeder let s = SSymbol $ case q of
bb2c1beb7ab66a49627a2a34df80864a3c65cc83Christian Maeder Universal -> "all"
bb2c1beb7ab66a49627a2a34df80864a3c65cc83Christian Maeder Existential -> "ex"
bb2c1beb7ab66a49627a2a34df80864a3c65cc83Christian Maeder Unique_existential -> "ex1"
bb2c1beb7ab66a49627a2a34df80864a3c65cc83Christian Maeder vl = SList $ map varDeclToSExpr $ flatVAR_DECLs vs
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder in SList [s, vl, f]
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder , foldJunction = \ _ j fs _ -> SList $ SSymbol (case j of
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Dis -> "or") : fs
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder , foldRelation = \ _ f1 c f2 _ -> SList
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder [ SSymbol (if c == Equivalence then "equiv" else "implies"), f1, f2]
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder , foldNegation = \ _ f _ -> SList [SSymbol "not", f]
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder , foldAtom = \ _ b _ -> SSymbol $ if b then "true" else "false"
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder , foldPredication = \ _ p ts _ ->
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder SList $ SSymbol "papply" : predToSSymbol sign p : ts
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder , foldDefinedness = \ _ t _ -> SList [SSymbol "def", t]
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder , foldEquation = \ _ t1 e t2 _ -> SList
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder [ SSymbol $ if e == Existl then "eeq" else "eq", t1, t2]
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder , foldMembership = \ _ t s _ ->
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder SList [SSymbol "member", t, sortToSSymbol s]
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldMixfix_formula = \ t _ -> sfail "Mixfix_formula" $ getRange t
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder , foldSort_gen_ax = \ _ cs b ->
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder let (srts, ops, _) = recover_Sort_gen_ax cs in
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder SList $ SSymbol ((if b then "freely-" else "") ++ "generated")
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder : (case srts of
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder [s] -> sortToSSymbol s
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder _ -> SList $ map sortToSSymbol srts)
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder : map (opToSSymbol sign) ops
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder , foldQuantOp = \ _ o _ _ -> sfail ("QuantOp " ++ show o) $ getRange o
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder , foldQuantPred = \ _ p _ _ -> sfail ("QuantPred " ++ show p) $ getRange p
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder , foldExtFORMULA = const mf
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder , foldQual_var = \ _ v _ _ ->
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder SList [SSymbol "varterm", varToSSymbol v]
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder , foldApplication = \ _ o ts _ ->
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder SList $ SSymbol "fapply" : opToSSymbol sign o : ts
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldSorted_term = \ _ r _ _ -> r
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder , foldCast = \ _ t s _ -> SList [SSymbol "cast", t, sortToSSymbol s]
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder , foldConditional = \ _ e f t _ -> SList [SSymbol "condition", e, f, t]
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder , foldMixfix_qual_pred = \ _ -> sfail "Mixfix_qual_pred" . getRange
f99c9fca932e8e6e8111049fd93164ed81e1b0abChristian Maeder , foldMixfix_term = \ t _ -> sfail "Mixfix_term" $ getRange t
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder , foldMixfix_token = \ _ -> sfail "Mixfix_token" . tokPos
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder , foldMixfix_sorted_term = \ _ _ -> sfail "Mixfix_sorted_term"
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder , foldMixfix_cast = \ _ _ -> sfail "Mixfix_cast"
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder , foldMixfix_parenthesized = \ _ _ -> sfail "Mixfix_parenthesized"
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder , foldMixfix_bracketed = \ _ _ -> sfail "Mixfix_bracketed"
6e538f8086fb560f0b88d49581f0006d6323bdc0Christian Maeder , foldMixfix_braced = \ _ _ -> sfail "Mixfix_braced"
6e538f8086fb560f0b88d49581f0006d6323bdc0Christian Maeder , foldExtTERM = const mf }
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian MaedersignToSExprs :: Sign a e -> [SExpr]
38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian MaedersignToSExprs sign = sortSignToSExprs sign
38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder : predMapToSExprs sign (predMap sign) ++ opMapToSExprs sign (opMap sign)
38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian MaedersortSignToSExprs :: Sign a e -> SExpr
38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian MaedersortSignToSExprs sign =
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder SList (SSymbol "sorts"
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder : map sortToSSymbol (Set.toList $ sortSet sign))
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederpredMapToSExprs :: Sign a e -> PredMap -> [SExpr]
05b9abe2e7d9e6126bf4ae29be6ef3693f32de73Christian MaederpredMapToSExprs sign =
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder map (\ (p, t) ->
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder SList [ SSymbol "predicate"
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder , predIdToSSymbol sign p t
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder , SList $ map sortToSSymbol $ predArgs t ])
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder . mapSetToList
13140d161d2d2d11d87283d01d57ee3a738a833dChristian MaederopMapToSExprs :: Sign a e -> OpMap -> [SExpr]
05b9abe2e7d9e6126bf4ae29be6ef3693f32de73Christian MaederopMapToSExprs sign =
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder map (\ (p, t) ->
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder SList [ SSymbol "function"
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder , opIdToSSymbol sign p t
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder , SList $ map sortToSSymbol $ opArgs t
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder , sortToSSymbol $ opRes t ])
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder . mapSetToList
05b9abe2e7d9e6126bf4ae29be6ef3693f32de73Christian MaedermorToSExprs :: Morphism f e m -> [SExpr]
05b9abe2e7d9e6126bf4ae29be6ef3693f32de73Christian MaedermorToSExprs m =
05b9abe2e7d9e6126bf4ae29be6ef3693f32de73Christian Maeder let src = msource m
05b9abe2e7d9e6126bf4ae29be6ef3693f32de73Christian Maeder tar = mtarget m
05b9abe2e7d9e6126bf4ae29be6ef3693f32de73Christian Maeder sm = sort_map m
05b9abe2e7d9e6126bf4ae29be6ef3693f32de73Christian Maeder in map (\ (s, t) -> SList [SSymbol "map", sortToSSymbol s, sortToSSymbol t])
a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder ++ Map.foldWithKey (\ i s -> case Set.toList s of
05b9abe2e7d9e6126bf4ae29be6ef3693f32de73Christian Maeder ot : _ -> let (j, nt) = mapOpSym sm (op_map m) (i, ot) in
05b9abe2e7d9e6126bf4ae29be6ef3693f32de73Christian Maeder if i == j then id else
05b9abe2e7d9e6126bf4ae29be6ef3693f32de73Christian Maeder (SList [ SSymbol "map", opIdToSSymbol src i ot
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder , opIdToSSymbol tar j nt] :)) []
a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder ++ Map.foldWithKey (\ i s -> case Set.toList s of
05b9abe2e7d9e6126bf4ae29be6ef3693f32de73Christian Maeder ot : _ -> let (j, nt) = mapPredSym sm (pred_map m) (i, ot) in
05b9abe2e7d9e6126bf4ae29be6ef3693f32de73Christian Maeder if i == j then id else
05b9abe2e7d9e6126bf4ae29be6ef3693f32de73Christian Maeder (SList [ SSymbol "map", predIdToSSymbol src i ot
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder , predIdToSSymbol tar j nt] :)) []
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder (MapSet.toMap $ predMap src)