content: {- |
  Module      :  ./VSE/ToSExpr.hs
  Description :  translate VSE 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 VSE to S-Expressions
  -}
  
  module VSE.ToSExpr where
  
  import VSE.As
  import VSE.Ana
  import VSE.Fold
  
  import CASL.AS_Basic_CASL
  import CASL.Fold
  import CASL.Sign
  import CASL.ToSExpr
  
  import Common.AS_Annotation
  import Common.Id
  import Common.LibName
  import Common.ProofUtils
  import Common.SExpr
  import qualified Common.Lib.MapSet as MapSet
  import qualified Common.Lib.Rel as Rel
  
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  import Data.Char (toLower)
  import Data.List (sortBy)
  import Data.Ord (comparing)
  
  addUniformRestr :: Sign f Procs -> [Named Sentence]
    -> (Sign f Procs, [Named Sentence])
  addUniformRestr sig nsens = let
    namedConstr = filter (\ ns -> case sentence ns of
                                  ExtFORMULA
                                   (Ranged
                                     (RestrictedConstraint {})
                                    _) -> True
                                  _ -> False ) nsens
    restrConstr = map sentence namedConstr
    restrToSExpr (procs, tSens)
                 (ExtFORMULA
                   (Ranged (RestrictedConstraint constrs restr _flag) _r)) =
     let
      (genSorts, genOps, _maps) = recover_Sort_gen_ax constrs
      genUniform sorts ops s = let
        hasResSort sn ~(Qual_op_name _ opType _) = res_OP_TYPE opType == sn
        argLength ~(Qual_op_name _ (Op_type _ args _ _) _) = length args
        ctors = sortBy (comparing argLength) $ filter (hasResSort s) ops
        genCodeForCtor ~(Qual_op_name ctor (Op_type _ args sn _) _) prg = let
          decls = genVars args
          vs = map (\ (i, a) -> Var_decl [i] a nullRange) decls
          recCalls = map (\ (i, x) ->
                           Ranged (Call (Predication
                                          (Qual_pred_name
                                            (gnUniformName s)
                                           (Pred_type [x] nullRange) nullRange)
                                          [Qual_var i x nullRange] nullRange
                                        )) nullRange) $
                     filter (flip elem sorts . snd) decls
          recCallsSeq = if null recCalls then Ranged Skip nullRange else
                        foldr1 (\ p1 p2 -> Ranged (Seq p1 p2) nullRange) recCalls
          in case recCalls of
           [] -> Ranged (
                  Block (Var_decl [yVar] s nullRange : vs)
                (Ranged (Seq
                  (Ranged
                     (Assign yVar (Qual_var xVar sn nullRange)
                      ) nullRange)
                  (Ranged (Seq (Ranged
                                     (Assign
                                       yVar
                                       (Application
                                        (Qual_op_name
                                        ctor
                                       (Op_type Partial args sn nullRange)
                                       nullRange)
                                        (map toQualVar vs)
                                        nullRange))
                                     nullRange)
                          (Ranged (If (mkStEq
                                 (mkAppl
                                   (
                                    mkQualOp
                                     (gnEqName s)
                                     (Op_type Partial [s, s]
                                      uBoolean nullRange)
                                   ) [mkVarTerm xVar s, mkVarTerm yVar s])
                                 aTrue)
                            (Ranged Skip nullRange)
                            prg) nullRange))
                  nullRange )) nullRange) ) nullRange
           _ -> Ranged (
                   Block (Var_decl [yVar] s nullRange : vs)
                  (Ranged (Seq (Ranged (Assign yVar
                                        (Qual_var xVar sn nullRange)
                                       ) nullRange)
                               (Ranged
                                (Seq recCallsSeq
                                 (Ranged (Seq
                                    (Ranged
                                      (Assign
                                        yVar
                                       (Application
                                        (Qual_op_name
                                       ctor
                                       (Op_type Partial args sn nullRange)
                                       nullRange)
                                        (map toQualVar vs)
                                        nullRange))
                                     nullRange)
                                  (Ranged (If (mkStEq
                                   ( mkAppl
                                   ( mkQualOp
                                     (gnEqName s)
                                     (Op_type Partial [s, s]
                                      uBoolean nullRange)
                                   ) [mkVarTerm xVar s, mkVarTerm yVar s])
                                  aTrue)
                                 (Ranged Skip nullRange) prg) nullRange))
                                 nullRange )) nullRange)) nullRange) ) nullRange
                               in
       [makeNamed "" $ ExtFORMULA $
       Ranged (Defprocs [
        Defproc Proc (gnUniformName s) [xVar]
        (Ranged (
          Block [] ( foldr genCodeForCtor (Ranged Abort nullRange)
                     ctors)
                ) nullRange
        )
        nullRange])
       nullRange,
       (makeNamed "" $
       Quantification Universal [Var_decl [xVar] s nullRange]
        (mkImpl
         ( ExtFORMULA $ Ranged
            (Dlformula Diamond ( Ranged
              (Call $ Predication
                (Qual_pred_name
                  (Map.findWithDefault (gnRestrName s) s restr)
                  (Pred_type [s] nullRange) nullRange)
                 [Qual_var xVar s nullRange] nullRange) nullRange)
              trueForm)
            nullRange)
         ( ExtFORMULA $ Ranged
            (Dlformula Diamond (Ranged
              (Call $ Predication
                (Qual_pred_name (gnUniformName s)
                  (Pred_type [s] nullRange) nullRange)
                 [Qual_var xVar s nullRange] nullRange) nullRange)
              trueForm)
            nullRange)) nullRange) {isAxiom = False}]
      procDefs = concatMap (genUniform genSorts genOps) genSorts
      procs' = Map.fromList $
               map (\ s -> (gnUniformName s,
                           Profile [Procparam In s] Nothing)) genSorts
     in
      (Map.union procs procs', tSens ++ procDefs)
    restrToSExpr _ _ = error "should not be anything than restricted constraints"
    (newProcs, trSens) = foldl restrToSExpr (Map.empty, []) restrConstr
                              in
   (sig {
     predMap = addMapSet (predMap sig) $ procsToPredMap $ Procs newProcs,
  
     extendedInfo = Procs $ Map.union newProcs (procsMap $ extendedInfo sig)},
    nameAndDisambiguate $
      trSens ++ filter (not . flip elem namedConstr) nsens)
  
  namedSenToSExpr :: Sign f Procs -> Named Sentence -> SExpr
  namedSenToSExpr sig ns =
    SList
      [ SSymbol "asentence"
      , SSymbol $ transString $ senAttr ns
      , SSymbol $ if isAxiom ns then "axiom" else "obligation"
      , SSymbol $ if isAxiom ns then "proved" else "open"
      , senToSExpr sig $ sentence ns ]
  
  senToSExpr :: Sign f Procs -> Sentence -> SExpr
  senToSExpr sig s = let ns = sentenceToSExpr sig s in case s of
      ExtFORMULA (Ranged (Defprocs _) _) ->
          SList [SSymbol "defprocs-sentence", ns]
      Sort_gen_ax _ _ ->
          SList [SSymbol "generatedness-sentence", ns]
      _ -> SList [SSymbol "formula-sentence", ns]
  
  sentenceToSExpr :: Sign f Procs -> Sentence -> SExpr
  sentenceToSExpr sign = let sig = addSig const sign boolSig in
    foldFormula $ sRec sig $ dlFormulaToSExpr sig
  
  dlFormulaToSExpr :: Sign f Procs -> Dlformula -> SExpr
  dlFormulaToSExpr sig = vseFormsToSExpr sig . unRanged
  
  vseFormsToSExpr :: Sign f Procs -> VSEforms -> SExpr
  vseFormsToSExpr sig vf = case vf of
    Dlformula b p s ->
      SList [SSymbol $ case b of
           Box -> "box"
           Diamond -> "diamond", progToSExpr sig p, sentenceToSExpr sig s]
    Defprocs ds ->
      SList $ SSymbol "defprocs" : map (defprocToSExpr sig) ds
    RestrictedConstraint {} ->
     error "restricted constraints should be handled separately"
  
  vDeclToSExpr :: Sign f Procs -> VarDecl -> SExpr
  vDeclToSExpr sig (VarDecl v s m _) =
    let vd@(SList [_, w, ty]) = varDeclToSExpr (v, s) in
    case m of
      Nothing -> vd
      Just trm -> SList [ SSymbol "vardecl", w, ty
                        , foldTerm (sRec sig $ error "vDeclToSExpr") trm ]
  
  procIdToSSymbol :: Sign f Procs -> Id -> SExpr
  procIdToSSymbol sig n = case lookupProc n sig of
          Nothing -> error "procIdToSSymbol"
          Just pr -> case profileToOpType pr of
            Just ot -> opIdToSSymbol sig n ot
            _ -> predIdToSSymbol sig n $ profileToPredType pr
  
  progToSExpr :: Sign f Procs -> Program -> SExpr
  progToSExpr sig = let
    pRec = sRec sig (error "progToSExpr")
    termToSExpr = foldTerm pRec
    formToSExpr = foldFormula pRec
    in foldProg FoldRec
    { foldAbort = const $ SSymbol "abort"
    , foldSkip = const $ SSymbol "skip"
    , foldAssign = \ _ v t ->
        SList [SSymbol "assign", varToSSymbol v, termToSExpr t]
    , foldCall = \ (Ranged _ r) f ->
        case f of
          Predication (Qual_pred_name i _ _) ts _ ->
            SList $ SSymbol "call" : procIdToSSymbol sig i : map termToSExpr ts
          _ -> sfail "Call" r
    , foldReturn = \ _ t -> SList [SSymbol "return", termToSExpr t]
    , foldBlock = \ ~(Ranged (Block vs p) _) _ _ ->
        let (vds, q) = addInits (toVarDecl vs) p
            ps = progToSExpr sig q
            nvs = map (vDeclToSExpr sig) vds
        in if null nvs then ps else SList [SSymbol "vblock", SList nvs, ps]
    , foldSeq = \ _ s1 s2 -> SList [SSymbol "seq", s1, s2]
    , foldIf = \ _ c s1 s2 -> SList [SSymbol "if", formToSExpr c, s1, s2]
    , foldWhile = \ _ c s -> SList [SSymbol "while", formToSExpr c, s] }
  
  defprocToSExpr :: Sign f Procs -> Defproc -> SExpr
  defprocToSExpr sig (Defproc k n vs p _) = SList
      [ SSymbol $ case k of
          Proc -> "defproc"
          Func -> "deffuncproc"
      , procIdToSSymbol sig n
      , SList $ map varToSSymbol vs
      , progToSExpr sig p ]
  
  paramToSExpr :: Procparam -> SExpr
  paramToSExpr (Procparam k s) = SList
    [ SSymbol $ map toLower $ show k
    , sortToSSymbol s ]
  
  procsToSExprs :: (Id -> Bool) -> Sign f Procs -> [SExpr]
  procsToSExprs f sig =
      map (\ (n, pr@(Profile as _)) -> case profileToOpType pr of
        Nothing -> SList
          [ SSymbol "procedure"
          , predIdToSSymbol sig n $ profileToPredType pr
          , SList $ map paramToSExpr as ]
        Just ot -> SList
          [ SSymbol "funcprocedure"
          , opIdToSSymbol sig n ot
          , SList $ map sortToSSymbol $ opArgs ot
          , sortToSSymbol $ opRes ot ])
      $ Map.toList $ Map.filterWithKey (\ i _ -> f i)
      $ procsMap $ extendedInfo sig
  
  vseSignToSExpr :: Sign f Procs -> SExpr
  vseSignToSExpr sig =
    let e = extendedInfo sig in
      SList $ SSymbol "signature" : sortSignToSExprs sig
        : predMapToSExprs sig (diffMapSet (predMap sig) $ procsToPredMap e)
        ++ opMapToSExprs sig (diffOpMapSet (opMap sig) $ procsToOpMap e)
        ++ procsToSExprs (const True) sig
  
  qualVseSignToSExpr :: SIMPLE_ID -> LibName -> Sign f Procs -> SExpr
  qualVseSignToSExpr nodeId libId sig =
    let e = extendedInfo sig in
      SList $ SSymbol "signature" : sortSignToSExprs sig
            { sortRel = Rel.delSet
              (Set.filter (not . isQualNameFrom nodeId libId) $ sortSet sig)
              $ sortRel sig }
        : predMapToSExprs sig
              (MapSet.filterWithKey (\ i _ -> isQualNameFrom nodeId libId i)
              . MapSet.difference (predMap sig) $ procsToPredMap e)
        ++ opMapToSExprs sig
              (MapSet.filterWithKey (\ i _ -> isQualNameFrom nodeId libId i)
              . diffOpMapSet (opMap sig) $ procsToOpMap e)
        ++ procsToSExprs (isQualNameFrom nodeId libId) sig
  