ToSExpr.hs revision e7b0b439ffae08514ac1afc62186d9a87ec6bd59
e9527d25af8ff3a40b1958aff04688d7df4e8e23ndModule : $Header$
fd9abdda70912b99b24e3bf1a38f26fde908a74cndDescription : translate CASL to S-Expressions
fd9abdda70912b99b24e3bf1a38f26fde908a74cndCopyright : (c) C. Maeder, DFKI 2008
fd9abdda70912b99b24e3bf1a38f26fde908a74cndLicense : similar to LGPL, see HetCATS/LICENSE.txt
e9527d25af8ff3a40b1958aff04688d7df4e8e23ndMaintainer : Christian.Maeder@dfki.de
e9527d25af8ff3a40b1958aff04688d7df4e8e23ndStability : provisional
e9527d25af8ff3a40b1958aff04688d7df4e8e23ndPortability : portable
e9527d25af8ff3a40b1958aff04688d7df4e8e23ndtranslation of CASL to S-Expressions
3f08db06526d6901aa08c110b5bc7dde6bc39905ndimport qualified Data.Map as Map
e9527d25af8ff3a40b1958aff04688d7df4e8e23ndimport qualified Data.Set as Set
f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjungimport qualified Data.List as List
e9527d25af8ff3a40b1958aff04688d7df4e8e23ndpredToSSymbol :: Sign f e -> PRED_SYMB -> SExpr
e9527d25af8ff3a40b1958aff04688d7df4e8e23ndpredToSSymbol sign p = case p of
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd Pred_name _ -> error "predToSSymbol"
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd Qual_pred_name i t _ -> case Map.lookup i $ predMap sign of
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd Nothing -> error "predToSSymbol2"
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd Just s -> case List.elemIndex (toPredType t) $ Set.toList s of
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd Nothing -> error "predToSSymbol3"
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd Just n -> idToSSymbol (n + 1) i
e9527d25af8ff3a40b1958aff04688d7df4e8e23ndopToSSymbol :: Sign f e -> OP_SYMB -> SExpr
e9527d25af8ff3a40b1958aff04688d7df4e8e23ndopToSSymbol sign o = case o of
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd Op_name _ -> error "opToSSymbol"
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd Qual_op_name i (Op_type _ args res _) _ ->
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd case Map.lookup i $ opMap sign of
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd Nothing -> error "opToSSymbol2"
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd Just s -> case List.findIndex
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd (\ r -> opArgs r == args && opRes r == res) $ Set.toList s of
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd Nothing -> error "opToSSymbol3"
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd Just n -> idToSSymbol (n + 1) i
e9527d25af8ff3a40b1958aff04688d7df4e8e23ndvarToSSymbol :: Token -> SExpr
e9527d25af8ff3a40b1958aff04688d7df4e8e23ndvarToSSymbol = SSymbol . transToken
e9527d25af8ff3a40b1958aff04688d7df4e8e23ndvarDeclToSExpr :: (VAR, SORT) -> SExpr
e9527d25af8ff3a40b1958aff04688d7df4e8e23ndvarDeclToSExpr (v, s) =
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd SList [SSymbol "vardecl-indet", varToSSymbol v, idToSSymbol 0 s]
e9527d25af8ff3a40b1958aff04688d7df4e8e23ndsfail :: String -> Range -> Result a
9a58dc6a2b26ec128b1270cf48810e705f1a90dbsfsfail s r = fatal_error ("unexpected " ++ s) r
e9527d25af8ff3a40b1958aff04688d7df4e8e23ndsRec :: Bool -> Sign a e -> (f -> Result SExpr)
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd -> Record f (Result SExpr) (Result SExpr)
e9527d25af8ff3a40b1958aff04688d7df4e8e23ndsRec withQuant sign mf = Record
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd { foldQuantification = \ _ q vs r p -> if withQuant then do
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd s <- case q of
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd Unique_existential -> sfail "Unique_existential" p
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd _ -> return $ SSymbol $ case q of
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd Universal -> "all"
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd Existential -> "ex"
9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf let vl = SList $ map varDeclToSExpr $ flatVAR_DECLs vs
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd return $ SList [s, vl, f]
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd else sfail "Quantification" p
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldConjunction = \ _ rs _ -> do
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd fs <- sequence rs
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd return $ SList $ SSymbol "and" : fs
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldDisjunction = \ _ rs _ -> do
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd fs <- sequence rs
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd return $ SList $ SSymbol "or" : fs
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldImplication = \ _ r1 r2 b _ -> do
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd return $ SList $ SSymbol "implies" : if b then [f1, f2] else [f2, f1]
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldEquivalence = \ _ r1 r2 _ -> do
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd return $ SList [SSymbol "equiv", f1, f2]
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldNegation = \ _ r _ -> do
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd return $ SList [SSymbol "not", f]
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldTrue_atom = \ _ _ -> return $ SSymbol "true"
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldFalse_atom = \ _ _ -> return $ SSymbol "false"
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldPredication = \ _ p rs _ -> do
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd ts <- sequence rs
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd return $ SList $ SSymbol "papply" : predToSSymbol sign p : ts
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldDefinedness = \ _ _ r -> sfail "Definedness" r
9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf , foldExistl_equation = \ _ _ _ r -> sfail "Existl_equation" r
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldStrong_equation = \ _ r1 r2 _ -> do
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd return $ SList [SSymbol "eq", t1, t2]
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldMembership = \ _ _ _ r -> sfail "Membership" r
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldMixfix_formula = \ t _ -> sfail "Mixfix_formula" $ getRange t
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldSort_gen_ax = \ _ _ _ -> sfail "Sort_gen_ax" nullRange
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldExtFORMULA = \ _ f -> mf f
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldSimpleId = \ _ t -> sfail "Simple_id" $ tokPos t
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldQual_var = \ _ v _ _ ->
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd return $ SList [SSymbol "varterm", varToSSymbol v]
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldApplication = \ _ o rs _ -> do
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd ts <- sequence rs
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd return $ SList $ SSymbol "fapply" : opToSSymbol sign o : ts
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldSorted_term = \ _ r _ _ -> r
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldCast = \ _ _ _ r -> sfail "Cast" r
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldConditional = \ _ _ _ _ r -> sfail "Conditional" r
30471a4650391f57975f60bbb6e4a90be7b284bfhumbedooh , foldMixfix_qual_pred = \ _ p -> sfail "Mixfix_qual_pred" $ getRange p
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldMixfix_term = \ (Mixfix_term ts) _ ->
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd sfail "Mixfix_term" $ getRange ts
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldMixfix_token = \ _ t -> sfail "Mixfix_token" $ tokPos t
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldMixfix_sorted_term = \ _ _ r -> sfail "Mixfix_sorted_term" r
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldMixfix_cast = \ _ _ r -> sfail "Mixfix_cast" r
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldMixfix_parenthesized = \ _ _ r -> sfail "Mixfix_parenthesized" r
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldMixfix_bracketed = \ _ _ r -> sfail "Mixfix_bracketed" r
e9527d25af8ff3a40b1958aff04688d7df4e8e23nd , foldMixfix_braced = \ _ _ r -> sfail "Mixfix_braced" r