content: {- |
  Module      :  ./THF/Translate.hs
  Description :  create legal THF mixfix identifier
  Copyright   :  (c) A. Tsogias, DFKI Bremen 2011
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Alexis.Tsogias@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  translate 'Id' to THF Constant
  -}
  
  module THF.Translate where
  
  import Common.Id
  import Common.Result
  
  import qualified Common.ProofUtils as CM (charMap)
  
  import HasCASL.Builtin
  import HasCASL.AsUtils
  
  import THF.As as THFAs
  
  import Data.Char
  import qualified Data.Map as Map
  
  
  mkTypesName :: THFAs.Constant -> THFAs.Name
  mkTypesName c = case c of
      A_Lower_Word w -> N_Atomic_Word $ A_Lower_Word
                       $ mkSimpleId ("type_" ++ show w)
      A_Single_Quoted s -> N_Atomic_Word $ A_Single_Quoted
                          $ mkSimpleId ("type_" ++ show s)
  
  mkConstsName :: THFAs.Constant -> THFAs.Name
  mkConstsName c = case c of
      A_Lower_Word w -> N_Atomic_Word $ A_Lower_Word
                       $ mkSimpleId ("const_" ++ show w)
      A_Single_Quoted s -> N_Atomic_Word $ A_Single_Quoted
                          $ mkSimpleId ("const_" ++ show s)
  
  mkDefName :: THFAs.Constant -> THFAs.Name
  mkDefName c = case c of
      A_Lower_Word w -> N_Atomic_Word $ A_Lower_Word
                       $ mkSimpleId ("def_" ++ show w)
      A_Single_Quoted s -> N_Atomic_Word $ A_Single_Quoted
                          $ mkSimpleId ("def_" ++ show s)
  
  transTypeId :: Id -> Result THFAs.Constant
  transTypeId id1 = case maybeElem id1 preDefHCTypeIds of
      Just res -> return $ stringToConstant res
      Nothing -> case transToTHFString $ show id1 of
          Just s -> return . A_Lower_Word . mkSimpleId $ "x_" ++ s
          Nothing -> fatal_error ("Unable to translate " ++ show id1 ++
              " into a THF valide Constant.") nullRange
  
  transAssumpId :: Id -> Result THFAs.Constant
  transAssumpId id1 = case maybeElem id1 preDefHCAssumpIds of
      Just res -> return $ stringToConstant res
      Nothing -> case transToTHFString $ show id1 of
          Just s -> return $ stringToConstant s
          Nothing -> fatal_error ("Unable to translate " ++ show id1 ++
              " into a THF valide Constant.") nullRange
  
  transAssumpsId :: Id -> Int -> Result THFAs.Constant
  transAssumpsId id1 int = if int == 1 then transAssumpId id1 else
      case transToTHFString $ show id1 of
          Just s -> return $ stringToConstant (s ++ show int)
          Nothing -> fatal_error ("Unable to translate " ++ show id1 ++
              " into a THF valide Constant.") nullRange
  
  stringToConstant :: String -> THFAs.Constant
  stringToConstant = A_Lower_Word . stringToLowerWord
  
  stringToLowerWord :: String -> Token
  stringToLowerWord = mkSimpleId . \ s -> case s of
     c : r -> if isLower c then s else 'x' : c : r
     "" -> ""
  
  stringToVariable :: String -> String
  stringToVariable s = case s of
     c : r -> if isUpper c then s else let d = toUpper c in d : 'x' : d : r
     "" -> ""
  
  transVarId :: Id -> Result Token
  transVarId id1 = case transToTHFString $ show id1 of
          Just s -> return $ mkSimpleId $ stringToVariable s
          Nothing -> fatal_error ("Unable to translate " ++ show id1 ++
              " into a THF valide Variable.") nullRange
  
  transToTHFString :: String -> Maybe String
  transToTHFString = transToTHFStringAux True
  
  transToTHFStringAux :: Bool -> String -> Maybe String
  transToTHFStringAux first s = case s of
      "" -> Just ""
      c : rc -> let
        x = 'x' -- escape character
        rest = transToTHFStringAux False rc
        in
          if isTHFChar c
          then if first && isDigit c || c == x then fmap ([x, c] ++) rest else
               fmap (c :) rest
          else case Map.lookup c charMap of
              Just res -> fmap (res ++) rest
              Nothing -> Nothing
  
  isTHFChar :: Char -> Bool
  isTHFChar c = isAlphaNum c && isAscii c || c == '_'
  
  isLowerTHFChar :: Char -> Bool
  isLowerTHFChar c = isLower c && isAscii c
  
  preDefHCTypeIds :: Map.Map Id String
  preDefHCTypeIds = Map.fromList
      [ (logId, "hct" ++ show logId)
      , (predTypeId, "hct" ++ show predTypeId)
      , (unitTypeId, "hct" ++ show unitTypeId)
      , (lazyTypeId, "hctLazy")
      , (arrowId FunArr, "hct__FunArr__")
      , (arrowId PFunArr, "hct__PFunArr__")
      , (arrowId ContFunArr, "hct__ContFunArr__")
      , (arrowId PContFunArr, "hct__PContFunArr__")
      , (productId 2 nullRange, "hct__X__")
      , (productId 3 nullRange, "hct__X__X__")
      , (productId 4 nullRange, "hct__X__X__X__")
      , (productId 5 nullRange, "hct__X__X__X__X__") ]
  
  preDefHCAssumpIds :: Map.Map Id String
  preDefHCAssumpIds = Map.fromList
      [ (botId, "hcc" ++ show botId)
      , (defId, "hcc" ++ show defId)
      , (notId, "hcc" ++ show notId)
      , (negId, "hccNeg__")
      , (whenElse, "hcc" ++ show whenElse)
      , (trueId, "hcc" ++ show trueId)
      , (falseId, "hcc" ++ show falseId)
      , (eqId, "hcc__Eq__")
      , (exEq, "hcc__ExEq__")
      , (resId, "hcc" ++ show resId)
      , (andId, "hcc__And__")
      , (orId, "hcc__Or__")
      , (eqvId, "hcc__Eqv__")
      , (implId, "hcc__Impl__")
      , (infixIf, "hcc" ++ show infixIf) ]
  
  maybeElem :: Id -> Map.Map Id a -> Maybe a
  maybeElem id1 m = helper id1 (Map.toList m)
      where
          helper :: Id -> [(Id, a)] -> Maybe a
          helper _ [] = Nothing
          helper id2 ((eid, ea) : r) =
              if myEqId id2 eid then Just ea else helper id2 r
  
  myEqId :: Id -> Id -> Bool
  myEqId (Id t1 c1 _) (Id t2 c2 _) = (t1, c1) == (t2, c2)
  
  -- | a separate Map speeds up lookup
  charMap :: Map.Map Char String
  charMap = Map.insert '\'' "Apostrophe"
    . Map.insert '.' "Dot"
    $ Map.map stringToVariable CM.charMap
    -- this map is no longer injective
  