hets/CASL/ToSExpr.hs

	ToSExpr.hs revision ca0d4947f7b0fdcbf7eac627659e6cff6d3863ba
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder{- |
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederModule      :  $Header$
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederDescription :  translate CASL to S-Expressions
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederCopyright   :  (c) C. Maeder, DFKI 2008
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederLicense     :  similar to LGPL, see HetCATS/LICENSE.txt
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederMaintainer  :  Christian.Maeder@dfki.de
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederStability   :  provisional
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederPortability :  portable
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maedertranslation of CASL to S-Expressions
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder-}
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maedermodule CASL.ToSExpr where
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maederimport CASL.Fold
bb4d3b6e93db1495f02de46aff5076862e30517bChristian Maederimport CASL.Morphism
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maederimport CASL.Sign
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maederimport CASL.AS_Basic_CASL
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maederimport CASL.Quantification
bb4d3b6e93db1495f02de46aff5076862e30517bChristian Maederimport Common.SExpr
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maederimport Common.Result
bb4d3b6e93db1495f02de46aff5076862e30517bChristian Maederimport Common.Id
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maederimport qualified Data.Map as Map
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maederimport qualified Data.Set as Set
bb4d3b6e93db1495f02de46aff5076862e30517bChristian Maederimport qualified Data.List as List
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder
21b18016469e574bd145ad07c7b0f02839677cc3Christian MaederpredToSSymbol :: Sign f e -> PRED_SYMB -> SExpr
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederpredToSSymbol sign p = case p of
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder    Pred_name _ -> error "predToSSymbol"
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder    Qual_pred_name i t _ -> predIdToSSymbol sign i $ toPredType t
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederpredIdToSSymbol :: Sign f e -> Id -> PredType -> SExpr
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederpredIdToSSymbol sign i t = case Map.lookup i $ predMap sign of
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder    Nothing -> error "predIdToSSymbol"
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder    Just s -> case List.elemIndex t $ Set.toList s of
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder      Nothing -> error "predIdToSSymbol2"
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder      Just n -> idToSSymbol (n + 1) i
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederopToSSymbol :: Sign f e -> OP_SYMB -> SExpr
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederopToSSymbol sign o = case o of
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder    Op_name _ -> error "opToSSymbol"
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder    Qual_op_name i t _ -> opIdToSSymbol sign i $ toOpType t
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederopIdToSSymbol :: Sign f e -> Id -> OpType -> SExpr
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederopIdToSSymbol sign i (OpType _ args res) = case Map.lookup i $ opMap sign of
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder    Nothing -> error $ "opIdToSSymbol " ++ show i
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder    Just s -> case List.findIndex
21b18016469e574bd145ad07c7b0f02839677cc3Christian Maeder      (\ r -> opArgs r == args && opRes r == res) $ Set.toList s of
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder        Nothing -> error "opIdToSSymbol2"
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder        Just n -> idToSSymbol (n + 1) i
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaedersortToSSymbol :: Id -> SExpr
7862e8fb34d79382e93b45ce894acdd928da8a51Christian MaedersortToSSymbol = idToSSymbol 0
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaedervarToSSymbol :: Token -> SExpr
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaedervarToSSymbol = SSymbol . transToken
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaedervarDeclToSExpr :: (VAR, SORT) -> SExpr
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaedervarDeclToSExpr (v, s) =
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder  SList [SSymbol "vardecl-indet", varToSSymbol v, sortToSSymbol s]
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maedersfail :: String -> Range -> a
7862e8fb34d79382e93b45ce894acdd928da8a51Christian Maedersfail s = error . show . Diag Error ("unexpected " ++ s)
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder
bb4d3b6e93db1495f02de46aff5076862e30517bChristian MaedersRec :: GetRange f => Sign a e -> (f -> SExpr) -> Record f SExpr SExpr
bb4d3b6e93db1495f02de46aff5076862e30517bChristian MaedersRec sign mf = Record
21b18016469e574bd145ad07c7b0f02839677cc3Christian Maeder    { foldQuantification = \ _ q vs f _ ->
21b18016469e574bd145ad07c7b0f02839677cc3Christian Maeder        let s = SSymbol $ case q of
21b18016469e574bd145ad07c7b0f02839677cc3Christian Maeder              Universal -> "all"
7862e8fb34d79382e93b45ce894acdd928da8a51Christian Maeder              Existential -> "ex"
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder              Unique_existential -> "ex1"
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder            vl = SList $ map varDeclToSExpr $ flatVAR_DECLs vs
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder        in SList [s, vl, f]
    , foldConjunction = \ _ fs _ -> SList $ SSymbol "and" : fs
    , foldDisjunction = \ _ fs _ -> SList $ SSymbol "or" : fs
    , foldImplication = \ _ f1 f2 b _ ->
        SList $ SSymbol "implies" : if b then [f1, f2] else [f2, f1]
    , foldEquivalence = \ _ f1 f2 _ -> SList [SSymbol "equiv", f1, f2]
    , foldNegation = \ _ f _ -> SList [SSymbol "not", f]
    , foldTrue_atom = \ _ _ -> SSymbol "true"
    , foldFalse_atom = \ _ _ -> SSymbol "false"
    , foldPredication = \ _ p ts _ ->
        SList $ SSymbol "papply" : predToSSymbol sign p : ts
    , foldDefinedness = \ _ t _ -> SList [SSymbol "def", t]
    , foldExistl_equation = \ _ t1 t2 _ -> SList [SSymbol "eeq", t1, t2]
    , foldStrong_equation = \ _ t1 t2 _ -> SList [SSymbol "eq", t1, t2]
    , foldMembership = \ _ t s _ ->
        SList [SSymbol "member", t, sortToSSymbol s]
    , foldMixfix_formula = \ t _ -> sfail "Mixfix_formula" $ getRange t
    , foldSort_gen_ax = \ _ cs b ->
      let (srts, ops, _) = recover_Sort_gen_ax cs in
      SList $ SSymbol ((if b then "freely-" else "") ++ "generated")
        : (case srts of
            [s] -> sortToSSymbol s
            _ -> SList $ map sortToSSymbol srts)
        : map (opToSSymbol sign) ops
    , foldExtFORMULA = \ _ f -> mf f
    , foldQual_var = \ _ v _ _ ->
        SList [SSymbol "varterm", varToSSymbol v]
    , foldApplication = \ _ o ts _ ->
        SList $ SSymbol "fapply" : opToSSymbol sign o : ts
    , foldSorted_term = \ _ r _ _ -> r
    , foldCast = \ _ t s _ -> SList [SSymbol "cast", t, sortToSSymbol s]
    , foldConditional = \ _ e f t _ -> SList [SSymbol "condition", e, f, t]
    , foldMixfix_qual_pred = \ _ p -> sfail "Mixfix_qual_pred" $ getRange p
    , foldMixfix_term = \ (Mixfix_term ts) _ ->
        sfail "Mixfix_term" $ getRange ts
    , foldMixfix_token = \ _ t -> sfail "Mixfix_token" $ tokPos t
    , foldMixfix_sorted_term = \ _ _ r -> sfail "Mixfix_sorted_term" r
    , foldMixfix_cast = \ _ _ r -> sfail "Mixfix_cast" r
    , foldMixfix_parenthesized = \ _ _ r -> sfail "Mixfix_parenthesized" r
    , foldMixfix_bracketed = \ _ _ r -> sfail "Mixfix_bracketed" r
    , foldMixfix_braced = \ _ _ r -> sfail "Mixfix_braced" r }

signToSExprs :: Sign a e -> [SExpr]
signToSExprs sign = sortSignToSExprs sign
  : predMapToSExprs sign (predMap sign) ++ opMapToSExprs sign (opMap sign)

sortSignToSExprs :: Sign a e -> SExpr
sortSignToSExprs sign =
    SList (SSymbol "sorts"
      : map sortToSSymbol (Set.toList $ sortSet sign))

predMapToSExprs :: Sign a e -> Map.Map Id (Set.Set PredType) -> [SExpr]
predMapToSExprs sign =
    concatMap (\ (p, ts) -> map (\ t ->
       SList [ SSymbol "predicate"
             , predIdToSSymbol sign p t
             , SList $ map sortToSSymbol $ predArgs t ]) $ Set.toList ts)
      . Map.toList

opMapToSExprs :: Sign a e -> OpMap -> [SExpr]
opMapToSExprs sign =
    concatMap (\ (p, ts) -> map (\ t ->
       SList [ SSymbol "function"
             , opIdToSSymbol sign p t
             , SList $ map sortToSSymbol $ opArgs t
             , sortToSSymbol $ opRes t ]) $ Set.toList ts)
      . Map.toList

morToSExprs :: Morphism f e m -> [SExpr]
morToSExprs m =
  let src = msource m
      tar = mtarget m
      sm = sort_map m
  in map (\ (s, t) -> SList [SSymbol "map", sortToSSymbol s, sortToSSymbol t])
     (Map.toList sm)
     ++ Map.foldWithKey (\ i s -> case Set.toList s of
          [] -> id
          ot : _ -> let (j, nt) = mapOpSym sm (op_map m) (i, ot) in
             if i == j then id else
               (SList [ SSymbol "map", opIdToSSymbol src i ot
                      , opIdToSSymbol tar j nt] :)) [] (opMap src)
     ++ Map.foldWithKey (\ i s -> case Set.toList s of
          [] -> id
          ot : _ -> let (j, nt) = mapPredSym sm (pred_map m) (i, ot) in
             if i == j then id else
               (SList [ SSymbol "map", predIdToSSymbol src i ot
                      , predIdToSSymbol tar j nt] :)) [] (predMap src)