{- |

Module : ./CASL/ToSExpr.hs

Description : translate CASL to S-Expressions

Copyright : (c) C. Maeder, DFKI 2008

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : portable

translation of CASL to S-Expressions

-}

module CASL.ToSExpr where

import CASL.Fold

import CASL.Morphism

import CASL.Sign

import CASL.AS_Basic_CASL

import CASL.Quantification

import Common.SExpr

import Common.Result

import Common.Id

import qualified Common.Lib.MapSet as MapSet

import Data.Function

import qualified Data.Map as Map

import qualified Data.Set as Set

import qualified Data.List as List

predToSSymbol :: Sign f e -> PRED_SYMB -> SExpr

predToSSymbol sign p = case p of

Pred_name _ -> error "predToSSymbol"

Qual_pred_name i t _ -> predIdToSSymbol sign i $ toPredType t

predIdToSSymbol :: Sign f e -> Id -> PredType -> SExpr

predIdToSSymbol sign i t =

case List.elemIndex t . Set.toList . MapSet.lookup i $ predMap sign of

Nothing -> error "predIdToSSymbol"

Just n -> idToSSymbol (n + 1) i

opToSSymbol :: Sign f e -> OP_SYMB -> SExpr

opToSSymbol sign o = case o of

Op_name _ -> error "opToSSymbol"

Qual_op_name i t _ -> opIdToSSymbol sign i $ toOpType t

opIdToSSymbol :: Sign f e -> Id -> OpType -> SExpr

opIdToSSymbol sign i t = case List.findIndex

(on (==) opSorts t) . Set.toList

. MapSet.lookup i $ opMap sign of

Nothing -> error $ "opIdToSSymbol " ++ show i

Just n -> idToSSymbol (n + 1) i

sortToSSymbol :: Id -> SExpr

sortToSSymbol = idToSSymbol 0

varToSSymbol :: Token -> SExpr

varToSSymbol = SSymbol . transToken

varDeclToSExpr :: (VAR, SORT) -> SExpr

varDeclToSExpr (v, s) =

SList [SSymbol "vardecl-indet", varToSSymbol v, sortToSSymbol s]

sfail :: String -> Range -> a

sfail s = error . show . Diag Error ("unexpected " ++ s)

sRec :: GetRange f => Sign a e -> (f -> SExpr) -> Record f SExpr SExpr

sRec sign mf = Record

{ foldQuantification = \ _ q vs f _ ->

let s = SSymbol $ case q of

Universal -> "all"

Existential -> "ex"

Unique_existential -> "ex1"

vl = SList $ map varDeclToSExpr $ flatVAR_DECLs vs

in SList [s, vl, f]

, foldJunction = \ _ j fs _ -> SList $ SSymbol (case j of

Con -> "and"

Dis -> "or") : fs

, foldRelation = \ _ f1 c f2 _ -> SList

[ SSymbol (if c == Equivalence then "equiv" else "implies"), f1, f2]

, foldNegation = \ _ f _ -> SList [SSymbol "not", f]

, foldAtom = \ _ b _ -> SSymbol $ if b then "true" else "false"

, foldPredication = \ _ p ts _ ->

SList $ SSymbol "papply" : predToSSymbol sign p : ts

, foldDefinedness = \ _ t _ -> SList [SSymbol "def", t]

, foldEquation = \ _ t1 e t2 _ -> SList

[ SSymbol $ if e == Existl then "eeq" else "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

, foldQuantOp = \ _ o _ _ -> sfail ("QuantOp " ++ show o) $ getRange o

, foldQuantPred = \ _ p _ _ -> sfail ("QuantPred " ++ show p) $ getRange p

, foldExtFORMULA = const mf

, 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 = \ _ -> sfail "Mixfix_qual_pred" . getRange

, foldMixfix_term = \ t _ -> sfail "Mixfix_term" $ getRange t

, foldMixfix_token = \ _ -> sfail "Mixfix_token" . tokPos

, foldMixfix_sorted_term = \ _ _ -> sfail "Mixfix_sorted_term"

, foldMixfix_cast = \ _ _ -> sfail "Mixfix_cast"

, foldMixfix_parenthesized = \ _ _ -> sfail "Mixfix_parenthesized"

, foldMixfix_bracketed = \ _ _ -> sfail "Mixfix_bracketed"

, foldMixfix_braced = \ _ _ -> sfail "Mixfix_braced"

, foldExtTERM = const mf }

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 -> PredMap -> [SExpr]

predMapToSExprs sign =

map (\ (p, t) ->

SList [ SSymbol "predicate"

, predIdToSSymbol sign p t

, SList $ map sortToSSymbol $ predArgs t ])

. mapSetToList

opMapToSExprs :: Sign a e -> OpMap -> [SExpr]

opMapToSExprs sign =

map (\ (p, t) ->

SList [ SSymbol "function"

, opIdToSSymbol sign p t

, SList $ map sortToSSymbol $ opArgs t

, sortToSSymbol $ opRes t ])

. mapSetToList

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] :)) []

(MapSet.toMap $ 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] :)) []

(MapSet.toMap $ predMap src)