{- |
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)
