content: {- |
  Module      :  ./Isabelle/Translate.hs
  Description :  create legal Isabelle mixfix identifier
  Copyright   :  (c) University of Cambridge, Cambridge, England
                 adaption (c) Till Mossakowski, Uni Bremen 2002-2005
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  translate 'Id' to Isabelle strings
  -}
  
  module Isabelle.Translate
      ( showIsaConstT, showIsaConstIT, showIsaTypeT, transConstStringT
      , transTypeStringT
      , mkIsaConstT, mkIsaConstIT, transString, isaPrelude
      , IsaPreludes (..)
      , getConstIsaToks ) where
  
  import Common.AS_Annotation
  import Common.GlobalAnnotations
  import Common.Id
  import Common.ProofUtils
  import Common.Utils
  import qualified Common.Lib.Rel as Rel
  
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  
  import Data.Char
  import Data.Maybe
  import Data.List
  
  import Isabelle.IsaSign
  import Isabelle.IsaConsts
  import Isabelle.IsaStrings
  
  -- ----------------- Id translation functions -------------------
  data IsaPreludes = IsaPreludes
    { preTypes :: Map.Map BaseSig (Set.Set String)
    , preConsts :: Map.Map BaseSig (Set.Set String) }
  
  isaKeyset :: Set.Set String
  isaKeyset = Set.fromList isaKeywords
  
  mkPreludeMap :: [(BaseSig, Set.Set String)] -> Map.Map BaseSig (Set.Set String)
  mkPreludeMap = Map.fromList . map (\ (b, s) -> (b, Set.union s isaKeyset))
  
  hc2isaNames :: [String]
  hc2isaNames =
    [ defOpS, "mapSnd", "mapFst", "lift2partial", "lift2bool"
    , "lift2unit", "liftUnit", "liftUnit2partial", "liftUnit2bool"
    , "liftUnit2unit", "bool2partial", "curryOp", "uncurryOp", "unpack2bool"
    , "partial2bool", "unpack2partial", "unpackBool", "unpackPartial"
    , "resOp", "whenElseOp", "exEqualOp", "existEqualOp", "ifImplOp", "flip"
    , "makePartial", "makeTotal", "noneOp", "strongEqualOp", "restrictOp"]
  
  isaPrelude :: IsaPreludes
  isaPrelude = IsaPreludes
    { preTypes = mkPreludeMap
        [ (HsHOL_thy, types mainS)
        , (HsHOLCF_thy, types holcfS)
        , (MainHC_thy, types mainS)
        , (MainHCPairs_thy, types mainS)
        , (Main_thy, types mainS)
        , (HOLCF_thy, types holcfS)]
    , preConsts = mkPreludeMap
        [ (HsHOL_thy, consts mainS)
        , (HsHOLCF_thy, Set.insert fliftbinS (consts holcfS))
        , (MainHC_thy, foldr Set.insert (consts mainS)
           $ [ pAppS, aptS, appS, pairC ] ++ hc2isaNames)
        , (MainHCPairs_thy, foldr Set.insert (consts mainS) hc2isaNames)
        , (Main_thy, consts mainS), (HOLCF_thy, consts holcfS)]}
  
  getAltTokenList :: String -> Int -> Id -> BaseSig -> [Token]
  getAltTokenList newPlace over i@(Id ms cs qs) thy = let
      (fs, ps) = splitMixToken ms
      nonPlaces = filter (not . isPlace) fs
      constSet = Map.findWithDefault Set.empty thy $ preConsts isaPrelude
      over2 = isSingle nonPlaces && Set.member (tokStr $ head nonPlaces)
              constSet || Set.member (show i) constSet
      o1 = if over2 && over == 0 then over + 1 else over
      newFs =
        let (fps, rts) = span isPlace fs in case rts of
          hd : tl | o1 > 0 -> fps ++ mkSimpleId (tokStr hd ++
              if o1 < 3 then replicate o1 '\'' else '_' : show o1)
                    : tl
          _ -> fs
      in getTokenList newPlace $ Id (newFs ++ ps) cs qs
  
  toAltSyntax :: Bool -> Int -> GlobalAnnos -> Int -> Id -> BaseSig
              -> Set.Set String -> Maybe AltSyntax
  toAltSyntax prd over ga n i thy toks = let
      (precMap, mx) = Rel.toPrecMap $ prec_annos ga
      minPrec = if prd then 42 else 52
      adjustPrec p = 2 * p + minPrec
      br = "/ "
      newPlace = br ++ "_"
      minL = replicate n lowPrio
      minL1 = tail minL
      minL2 = tail minL1
      ni = placeCount i
      atoks@(hd : tl) = getAltTokenList newPlace over i thy
      compoundToks = map (: []) ",[]{}"
      convert Token { tokStr = s } =
        if elem s $ newPlace : compoundToks then s else br ++ quote s
      tts = concatMap convert tl
      ht = let chd = convert hd in
        if isPrefixOf br chd then drop (length br) chd else chd
      ts = ht ++ tts
      (precList, erg)
        | isInfix i = case Map.lookup i precMap of
          Just p -> let
              q = adjustPrec p
              (l, r) = case Map.lookup i $ assoc_annos ga of
                   Nothing -> (q + 1, q + 1)
                   Just ALeft -> (q, q + 1)
                   Just ARight -> (q + 1, q)
              in (l : minL2 ++ [r], q)
          Nothing -> let q = adjustPrec $ mx + 1 in (q : minL2 ++ [q], minPrec)
        | begPlace i = let q = adjustPrec $ mx + 3 in (q : minL1 , q)
        | endPlace i = let q = adjustPrec $ mx + 2 in (minL1 ++ [q], q)
        | otherwise = (minL, maxPrio - 1)
      in if n < 0 || ni > 1 && ni /= n
             || any (flip Set.member toks . tokStr) atoks then Nothing
         else Just $ if n == 0 then AltSyntax ts [] maxPrio
         else if isMixfix i then AltSyntax
                  ('(' : ts ++ ")") precList erg
         else AltSyntax
              (ts ++ "/'(" ++
                     concat (replicate (n - 1) "_,/ ")
                     ++ "_')") (replicate n 3) $ maxPrio - 1
  
  quote :: String -> String
  quote l = case l of
      [] -> l
      c : r -> (if elem c "_/'()" then '\'' : [c]
                else if elem c "\\\"" then '\\' : [c] else [c]) ++ quote r
  
  showIsaT1 :: (String -> String) -> Id -> String
  showIsaT1 tr ide = let
      str = tr $ show ide
      in if null str then error "showIsaT1" else if
         elem (last str) "_" then str ++ "X" else str
  
  showIsaConstT :: Id -> BaseSig -> String
  showIsaConstT ide thy = showIsaT1 (transConstStringT thy) ide
  
  -- also pass number of arguments
  mkIsaConstT :: Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> Set.Set String
              -> VName
  mkIsaConstT = mkIsaConstVName 0 showIsaConstT
  
  mkIsaConstVName :: Int -> (Id -> BaseSig -> String) -> Bool -> GlobalAnnos
                  -> Int -> Id -> BaseSig -> Set.Set String -> VName
  mkIsaConstVName over f prd ga n ide thy toks =
    let s = f ide thy
        a = toAltSyntax prd over ga n ide thy toks
   in if n == 0 && case a of
        Just (AltSyntax as [] _) -> as == s
        _ -> False then VName { new = s, altSyn = Nothing }
      else VName
    { new = (if n < 0 || isMixfix ide || s /= show ide then id else ("X_" ++)) s
    , altSyn = a }
  
  showIsaTypeT :: Id -> BaseSig -> String
  showIsaTypeT ide thy = showIsaT1 (transTypeStringT thy) ide
  
  -- | add a number for overloading
  showIsaConstIT :: Id -> Int -> BaseSig -> String
  showIsaConstIT ide i thy = showIsaConstT ide thy ++ "X" ++ show i
  
  mkIsaConstIT :: Bool -> GlobalAnnos -> Int -> Id -> Int -> BaseSig
               -> Set.Set String -> VName
  mkIsaConstIT prd ga n ide i =
      mkIsaConstVName i (`showIsaConstIT` i) prd ga n ide
  
  {- | get the tokens of the alternative syntax that should not be used
       as variables -}
  getConstIsaToks :: Id -> Int -> BaseSig -> Set.Set String
  getConstIsaToks ide i thy = if i < 2 then
     Set.union (getConstIsaToksAux ide 0 thy) (getConstIsaToksAux ide 1 thy)
     else getConstIsaToksAux ide i thy
  
  getConstIsaToksAux :: Id -> Int -> BaseSig -> Set.Set String
  getConstIsaToksAux ide i =
     foldr (Set.insert . tokStr)
               Set.empty . getAltTokenList "" i ide
  
  transIsaInternalName :: String -> String
  transIsaInternalName s = if last s == '_' then s ++ "X" else s
  
  transIsaStringT :: Map.Map BaseSig (Set.Set String) -> BaseSig
                  -> String -> String
  transIsaStringT m i s = let t = transStringAux False s in
    transIsaInternalName $ if Set.member t
      $ fromMaybe (error "Isabelle.transIsaStringT") $ Map.lookup i m
    then transIsaStringT m i $ '_' : s else t
  
  transConstStringT :: BaseSig -> String -> String
  transConstStringT = transIsaStringT $ preConsts isaPrelude
  
  transTypeStringT :: BaseSig -> String -> String
  transTypeStringT = transIsaStringT $ preTypes isaPrelude
  
  -- | check for legal alphanumeric Isabelle characters
  isIsaChar :: Char -> Bool
  isIsaChar c = isAlphaNum c && isAscii c || elem c "_'"
  
  -- | translate to a valid Isabelle string possibly non-injectively
  transString :: String -> String
  transString = transStringAux True
  
  -- | if true don't try to be injective
  transStringAux :: Bool -> String -> String
  transStringAux b str = let
      x = 'X'
      replaceChar1 d | not b && d == x = [x, x]  -- code out existing X!
                     | b && d == ' ' = "_"
                     | isIsaChar d = [d]
                     | otherwise = x : replaceChar d
      in case str of
      "" -> error "transString"
      c : s -> let l = replaceChar1 c in
               (if isDigit c || elem c "_'" then [x, c]
               else l) ++ concatMap replaceChar1
          (if b then replace "' '" "'Space'" s else s)
  
  -- | injective replacement of special characters
  replaceChar :: Char -> String
  -- <http://www.htmlhelp.com/reference/charset/>
  replaceChar c = if isIsaChar c then [c] else let n = ord c in
      if n <= 32 || n >= 127 && n < 160 || n > 255 then "Slash_" ++ show n
      else lookupCharMap c
  