ToSExpr.hs revision 05b9abe2e7d9e6126bf4ae29be6ef3693f32de73
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndModule : $Header$
fd9abdda70912b99b24e3bf1a38f26fde908a74cndDescription : translate CASL to S-Expressions
fd9abdda70912b99b24e3bf1a38f26fde908a74cndCopyright : (c) C. Maeder, DFKI 2008
fd9abdda70912b99b24e3bf1a38f26fde908a74cndLicense : similar to LGPL, see HetCATS/LICENSE.txt
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndMaintainer : Christian.Maeder@dfki.de
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndStability : provisional
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndPortability : portable
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndtranslation of CASL to S-Expressions
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndimport qualified Data.Map as Map
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndimport qualified Data.Set as Set
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndimport qualified Data.List as List
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndpredToSSymbol :: Sign f e -> PRED_SYMB -> SExpr
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndpredToSSymbol sign p = case p of
d474d8ef01ec5c2a09341cd148851ed383c3287crbowen Pred_name _ -> error "predToSSymbol"
d474d8ef01ec5c2a09341cd148851ed383c3287crbowen Qual_pred_name i t _ -> predIdToSSymbol sign i $ toPredType t
e34c72770fb8ee6b2903f29a0c86c0d0509eefa8igalicpredIdToSSymbol :: Sign f e -> Id -> PredType -> SExpr
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndpredIdToSSymbol sign i t = case Map.lookup i $ predMap sign of
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd Nothing -> error "predIdToSSymbol"
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd Nothing -> error "predIdToSSymbol2"
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd Just n -> idToSSymbol (n + 1) i
30471a4650391f57975f60bbb6e4a90be7b284bfhumbedoohopToSSymbol :: Sign f e -> OP_SYMB -> SExpr
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndopToSSymbol sign o = case o of
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd Op_name _ -> error "opToSSymbol"
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd Qual_op_name i t _ -> opIdToSSymbol sign i $ toOpType t
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndopIdToSSymbol :: Sign f e -> Id -> OpType -> SExpr
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndopIdToSSymbol sign i (OpType _ args res) = case Map.lookup i $ opMap sign of
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd Nothing -> error $ "opIdToSSymbol " ++ show i
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd Just s -> case List.findIndex
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd (\ r -> opArgs r == args && opRes r == res) $ Set.toList s of
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd Nothing -> error "opIdToSSymbol2"
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd Just n -> idToSSymbol (n + 1) i
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndsortToSSymbol :: Id -> SExpr
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndsortToSSymbol = idToSSymbol 0
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndvarToSSymbol :: Token -> SExpr
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndvarToSSymbol = SSymbol . transToken
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndvarDeclToSExpr :: (VAR, SORT) -> SExpr
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndvarDeclToSExpr (v, s) =
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd SList [SSymbol "vardecl-indet", varToSSymbol v, sortToSSymbol s]
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndsfail :: String -> Range -> a
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndsfail s = error . show . Diag Error ("unexpected " ++ s)
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndsRec :: Sign a e -> (f -> SExpr)
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd -> Record f SExpr SExpr
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndsRec sign mf = Record
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd { foldQuantification = \ _ q vs f _ ->
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd let s = SSymbol $ case q of
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd Universal -> "all"
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd Existential -> "ex"
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd Unique_existential -> "ex1"
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd vl = SList $ map varDeclToSExpr $ flatVAR_DECLs vs
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd in SList [s, vl, f]
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldConjunction = \ _ fs _ -> SList $ SSymbol "and" : fs
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldDisjunction = \ _ fs _ -> SList $ SSymbol "or" : fs
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldImplication = \ _ f1 f2 b _ ->
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd SList $ SSymbol "implies" : if b then [f1, f2] else [f2, f1]
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldEquivalence = \ _ f1 f2 _ -> SList [SSymbol "equiv", f1, f2]
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldNegation = \ _ f _ -> SList [SSymbol "not", f]
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldTrue_atom = \ _ _ -> SSymbol "true"
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldFalse_atom = \ _ _ -> SSymbol "false"
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldPredication = \ _ p ts _ ->
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd SList $ SSymbol "papply" : predToSSymbol sign p : ts
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldDefinedness = \ _ t _ -> SList [SSymbol "def", t]
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldExistl_equation = \ _ t1 t2 _ -> SList [SSymbol "eeq", t1, t2]
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldStrong_equation = \ _ t1 t2 _ -> SList [SSymbol "eq", t1, t2]
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldMembership = \ _ t s _ ->
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd SList [SSymbol "member", t, sortToSSymbol s]
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldMixfix_formula = \ t _ -> sfail "Mixfix_formula" $ getRange t
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldSort_gen_ax = \ _ cs b ->
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd let (srts, ops, _) = recover_Sort_gen_ax cs in
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd SList $ SSymbol ((if b then "freely-" else "") ++ "generated")
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd : (case srts of
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd [s] -> sortToSSymbol s
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd _ -> SList $ map sortToSSymbol srts)
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd : map (opToSSymbol sign) ops
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldExtFORMULA = \ _ f -> mf f
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldQual_var = \ _ v _ _ ->
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd SList [SSymbol "varterm", varToSSymbol v]
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldApplication = \ _ o ts _ ->
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd SList $ SSymbol "fapply" : opToSSymbol sign o : ts
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldSorted_term = \ _ r _ _ -> r
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldCast = \ _ t s _ -> SList [SSymbol "cast", t, sortToSSymbol s]
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldConditional = \ _ e f t _ -> SList [SSymbol "condition", e, f, t]
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldMixfix_qual_pred = \ _ p -> sfail "Mixfix_qual_pred" $ getRange p
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldMixfix_term = \ (Mixfix_term ts) _ ->
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd sfail "Mixfix_term" $ getRange ts
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldMixfix_token = \ _ t -> sfail "Mixfix_token" $ tokPos t
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldMixfix_sorted_term = \ _ _ r -> sfail "Mixfix_sorted_term" r
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldMixfix_cast = \ _ _ r -> sfail "Mixfix_cast" r
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldMixfix_parenthesized = \ _ _ r -> sfail "Mixfix_parenthesized" r
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldMixfix_bracketed = \ _ _ r -> sfail "Mixfix_bracketed" r
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , foldMixfix_braced = \ _ _ r -> sfail "Mixfix_braced" r }
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndsignToSExprs :: Sign a e -> [SExpr]
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndsignToSExprs sign = sortSignToSExprs sign
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd : predMapToSExprs sign (predMap sign) ++ opMapToSExprs sign (opMap sign)
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndsortSignToSExprs :: Sign a e -> SExpr
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndsortSignToSExprs sign =
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd SList (SSymbol "sorts"
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd : map sortToSSymbol (Set.toList $ sortSet sign))
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndpredMapToSExprs :: Sign a e -> Map.Map Id (Set.Set PredType) -> [SExpr]
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndpredMapToSExprs sign =
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd concatMap (\ (p, ts) -> map (\ t ->
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd SList [ SSymbol "predicate"
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , predIdToSSymbol sign p t
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , SList $ map sortToSSymbol $ predArgs t ]) $ Set.toList ts)
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndopMapToSExprs :: Sign a e -> OpMap -> [SExpr]
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndopMapToSExprs sign =
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd concatMap (\ (p, ts) -> map (\ t ->
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd SList [ SSymbol "function"
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , opIdToSSymbol sign p t
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , SList $ map sortToSSymbol $ opArgs t
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , sortToSSymbol $ opRes t ]) $ Set.toList ts)
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndmorToSExprs :: Morphism f e m -> [SExpr]
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndmorToSExprs m =
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd let src = msource m
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd tar = mtarget m
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd sm = sort_map m
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd in map (\ (s, t) -> SList [SSymbol "map", sortToSSymbol s, sortToSSymbol t])
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd ot : _ -> let (j, nt) = mapOpSym sm (op_map m) (i, ot) in
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd if i == j then id else
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd (SList [ SSymbol "map", opIdToSSymbol src i ot
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd , opIdToSSymbol tar j nt] :)) [] (opMap src)
727872d18412fc021f03969b8641810d8896820bhumbedooh ot : _ -> let (j, nt) = mapPredSym sm (pred_map m) (i, ot) in
0d0ba3a410038e179b695446bb149cce6264e0abnd if i == j then id else
727872d18412fc021f03969b8641810d8896820bhumbedooh (SList [ SSymbol "map", predIdToSSymbol src i ot
cc7e1025de9ac63bd4db6fe7f71c158b2cf09fe4humbedooh , predIdToSSymbol tar j nt] :)) [] (predMap src)