ToSExpr.hs revision 7fe976d9f9c4af1aa7636c568d9919859523de0a
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederModule : $Header$
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederDescription : translate CASL to S-Expressions
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederCopyright : (c) C. Maeder, DFKI 2008
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederMaintainer : Christian.Maeder@dfki.de
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederStability : provisional
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederPortability : portable
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maedertranslation of CASL to S-Expressions
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
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian MaederpredIdToSSymbol sign i t = case Map.lookup i $ predMap sign of
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder Nothing -> error "predIdToSSymbol"
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder Just s -> case List.elemIndex t $ Set.toList s of
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder Nothing -> error "predIdToSSymbol2"
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder Just n -> idToSSymbol (n + 1) i
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaederopToSSymbol :: Sign f e -> OP_SYMB -> SExpr
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian 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
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian MaederopIdToSSymbol sign i (OpType _ args res) = case Map.lookup i $ opMap sign of
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder Nothing -> error "opIdToSSymbol"
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder (\ r -> opArgs r == args && opRes r == res) $ Set.toList s of
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder Nothing -> error "opIdToSSymbol2"
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]
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maedersfail :: String -> Range -> Result a
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maedersfail s r = fatal_error ("unexpected " ++ s) r
a94f7b3982dccd2e01bd87f64de1aeab6edac118Christian MaedersRec :: Bool -> Sign a e -> (f -> Result SExpr)
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder -> Record f (Result SExpr) (Result SExpr)
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaedersRec withQuant sign mf = Record
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder { foldQuantification = \ _ q vs r p -> if withQuant then do
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder s <- case q of
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder Unique_existential -> sfail "Unique_existential" p
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder _ -> return $ SSymbol $ case q of
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder Universal -> "all"
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder Existential -> "ex"
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder let vl = SList $ map varDeclToSExpr $ flatVAR_DECLs vs
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder return $ SList [s, vl, f]
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder else sfail "Quantification" p
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldConjunction = \ _ rs _ -> do
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder fs <- sequence rs
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder return $ SList $ SSymbol "and" : fs
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldDisjunction = \ _ rs _ -> do
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder fs <- sequence rs
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder return $ SList $ SSymbol "or" : fs
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldImplication = \ _ r1 r2 b _ -> do
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder return $ SList $ SSymbol "implies" : if b then [f1, f2] else [f2, f1]
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldEquivalence = \ _ r1 r2 _ -> do
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder return $ SList [SSymbol "equiv", f1, f2]
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldNegation = \ _ r _ -> do
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder return $ SList [SSymbol "not", f]
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldTrue_atom = \ _ _ -> return $ SSymbol "true"
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldFalse_atom = \ _ _ -> return $ SSymbol "false"
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldPredication = \ _ p rs _ -> do
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder ts <- sequence rs
e7b0b439ffae08514ac1afc62186d9a87ec6bd59Christian Maeder return $ SList $ SSymbol "papply" : predToSSymbol sign p : ts
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldDefinedness = \ _ _ r -> sfail "Definedness" r
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldExistl_equation = \ _ _ _ r -> sfail "Existl_equation" r
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldStrong_equation = \ _ r1 r2 _ -> do
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder return $ SList [SSymbol "eq", t1, t2]
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldMembership = \ _ _ _ r -> sfail "Membership" r
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
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder return $ 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
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldExtFORMULA = \ _ f -> mf f
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldSimpleId = \ _ t -> sfail "Simple_id" $ tokPos t
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder , foldQual_var = \ _ v _ _ ->
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder return $ SList [SSymbol "varterm", varToSSymbol v]
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldApplication = \ _ o rs _ -> do
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder ts <- sequence rs
e7b0b439ffae08514ac1afc62186d9a87ec6bd59Christian Maeder return $ SList $ SSymbol "fapply" : opToSSymbol sign o : ts
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldSorted_term = \ _ r _ _ -> r
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldCast = \ _ _ _ r -> sfail "Cast" r
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldConditional = \ _ _ _ _ r -> sfail "Conditional" r
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldMixfix_qual_pred = \ _ p -> sfail "Mixfix_qual_pred" $ getRange p
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldMixfix_term = \ (Mixfix_term ts) _ ->
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder sfail "Mixfix_term" $ getRange ts
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldMixfix_token = \ _ t -> sfail "Mixfix_token" $ tokPos t
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldMixfix_sorted_term = \ _ _ r -> sfail "Mixfix_sorted_term" r
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldMixfix_cast = \ _ _ r -> sfail "Mixfix_cast" r
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldMixfix_parenthesized = \ _ _ r -> sfail "Mixfix_parenthesized" r
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldMixfix_bracketed = \ _ _ r -> sfail "Mixfix_bracketed" r
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldMixfix_braced = \ _ _ r -> sfail "Mixfix_braced" r
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian MaedersignToSExprs :: Sign a e -> [SExpr]
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian MaedersignToSExprs sign =
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder SList (SSymbol "sorts"
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder : map sortToSSymbol (Set.toList $ sortSet sign))
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder : concatMap (\ (p, ts) -> map (\ t ->
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder SList [ SSymbol "predicate"
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder , predIdToSSymbol sign p t
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder , SList $ map sortToSSymbol $ predArgs t ]) $ Set.toList ts)
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder (Map.toList $ predMap sign)
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder ++ concatMap (\ (p, ts) -> map (\ t ->
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder SList [ SSymbol "function"
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder , opIdToSSymbol sign p t
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder , SList $ map sortToSSymbol $ opArgs t
0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder , sortToSSymbol $ opRes t ]) $ Set.toList ts)