content: {-# LANGUAGE FlexibleInstances #-}
  {- |
  Module      :  ./Omega/ToLisp.hs
  Description :  Omega Lisp Output
  Copyright   :  (c) Ewaryst Schulz, DFKI 2008
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Ewaryst.Schulz@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  The Lisp interface
  -}
  module Omega.ToLisp ( printLibrary ) where
  
  import Data.List
  import qualified Data.Map as Map
  
  import Omega.DataTypes
  
  data PrintEnvironment = Env { library :: String, theory :: String }
  
  class SExprPrintable a where
    -- | Render instance to an SExpression string.
    toSExpr :: PrintEnvironment -> a -> String
  
  emptyEnv :: PrintEnvironment
  emptyEnv = Env "" ""
  
  
  -- * THEORY HANDLING
  
  theoremFun :: Bool -> String
  theoremFun True = "theory:add-conjecture"
  theoremFun False = "theory:add-axiom"
  
  theoryFun :: String
  theoryFun = "theory:add-theory"
  
  symbolFun :: String
  symbolFun = "theory:add-symbol"
  
  
  -- | Outputs a library to omega's lisp format.
  printLibrary :: Library -> String
  printLibrary = toSExpr emptyEnv
  
  instance SExprPrintable Library where
      toSExpr e (Library name theories) =
          let e' = e {library = name}
              in unlines $ map (toSExpr e') theories
  
  instance SExprPrintable Theory where
      toSExpr e (Theory name imports items) =
          let e' = e {theory = name}
          in unlines $ toSExpr e' (theoryFun : show name : map show imports)
                                 : map (toSExpr e') items
  
  instance SExprPrintable TCElement where
      toSExpr e (TCAxiomOrTheorem isTheorem name formula) =
          toSExpr e [theoremFun isTheorem, show name,
                     show $ printTerm formula, show $ theory e]
      toSExpr e (TCSymbol name) = toSExpr e [symbolFun, show name, show $ theory e]
  -- toSExpr e (TCComment comment) = ""
      toSExpr _ _ = ""
  
  instance SExprPrintable [String] where
      toSExpr _ l = "(" ++ unwords l ++ ")"
  
  -- * TERM HANDLING
  
  data SymbolFormat = Infix | Other deriving (Show, Eq, Ord)
  
  -- | Omegas built in symbols
  symbolMap :: Map.Map String (Term, SymbolFormat)
  symbolMap = Map.fromList [("__/\\__", (Symbol "/\\", Infix)),
                            ("__\\/__", (Symbol "\\/", Infix)),
                            ("__=>__", (Symbol "=>", Infix)),
                            ("__<=>__", (Symbol "<=>", Infix)),
                            ("__=__", (Symbol "=", Infix)),
                            ("not__", (Symbol "~", Other))]
  
  symbolLookup :: Term -> Maybe (Term, SymbolFormat)
  symbolLookup (Symbol name) = Map.lookup name symbolMap
  symbolLookup _ = Nothing
  
  printTerm :: Term -> String
  printTerm (Symbol name) = name
  printTerm (Var name) = name
  printTerm (App _ []) =
      error "printTerm: application to zero arguments!"
  printTerm (App fun args) =
      let mapped = symbolLookup fun
      in case mapped of
           Nothing -> concat [printTerm fun, "(", concatSTL args, ")"]
           Just (t, Infix) -> concat ["(", printTerm (head args), " ",
                                     printTerm t, " ", printTerm (args !! 1), ")"]
           Just (t, _) -> concat [printTerm t, "(", concatSTL args, ")"]
  printTerm (Bind binder vars body) =
      concat ["(", binder, " ", concatSTL vars, ". ", printTerm body, ")"]
  
  concatSTL :: [Term] -> String
  concatSTL l = intercalate "," (map printTerm l)
  