{- |
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
  { IsaPreludes -> Map BaseSig (Set String)
preTypes :: Map.Map BaseSig (Set.Set String)
  , IsaPreludes -> Map BaseSig (Set String)
preConsts :: Map.Map BaseSig (Set.Set String) }

isaKeyset :: Set.Set String
isaKeyset :: Set String
isaKeyset = [String] -> Set String
forall a. Ord a => [a] -> Set a
Set.fromList [String]
isaKeywords

mkPreludeMap :: [(BaseSig, Set.Set String)] -> Map.Map BaseSig (Set.Set String)
mkPreludeMap :: [(BaseSig, Set String)] -> Map BaseSig (Set String)
mkPreludeMap = [(BaseSig, Set String)] -> Map BaseSig (Set String)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(BaseSig, Set String)] -> Map BaseSig (Set String))
-> ([(BaseSig, Set String)] -> [(BaseSig, Set String)])
-> [(BaseSig, Set String)]
-> Map BaseSig (Set String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((BaseSig, Set String) -> (BaseSig, Set String))
-> [(BaseSig, Set String)] -> [(BaseSig, Set String)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (b :: BaseSig
b, s :: Set String
s) -> (BaseSig
b, Set String -> Set String -> Set String
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set String
s Set String
isaKeyset))

hc2isaNames :: [String]
hc2isaNames :: [String]
hc2isaNames =
  [ String
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
isaPrelude = IsaPreludes :: Map BaseSig (Set String) -> Map BaseSig (Set String) -> IsaPreludes
IsaPreludes
  { preTypes :: Map BaseSig (Set String)
preTypes = [(BaseSig, Set String)] -> Map BaseSig (Set String)
mkPreludeMap
      [ (BaseSig
HsHOL_thy, IsaSets -> Set String
types IsaSets
mainS)
      , (BaseSig
HsHOLCF_thy, IsaSets -> Set String
types IsaSets
holcfS)
      , (BaseSig
MainHC_thy, IsaSets -> Set String
types IsaSets
mainS)
      , (BaseSig
MainHCPairs_thy, IsaSets -> Set String
types IsaSets
mainS)
      , (BaseSig
Main_thy, IsaSets -> Set String
types IsaSets
mainS)
      , (BaseSig
HOLCF_thy, IsaSets -> Set String
types IsaSets
holcfS)]
  , preConsts :: Map BaseSig (Set String)
preConsts = [(BaseSig, Set String)] -> Map BaseSig (Set String)
mkPreludeMap
      [ (BaseSig
HsHOL_thy, IsaSets -> Set String
consts IsaSets
mainS)
      , (BaseSig
HsHOLCF_thy, String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert String
fliftbinS (IsaSets -> Set String
consts IsaSets
holcfS))
      , (BaseSig
MainHC_thy, (String -> Set String -> Set String)
-> Set String -> [String] -> Set String
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert (IsaSets -> Set String
consts IsaSets
mainS)
         ([String] -> Set String) -> [String] -> Set String
forall a b. (a -> b) -> a -> b
$ [ String
pAppS, String
aptS, String
appS, String
pairC ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
hc2isaNames)
      , (BaseSig
MainHCPairs_thy, (String -> Set String -> Set String)
-> Set String -> [String] -> Set String
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert (IsaSets -> Set String
consts IsaSets
mainS) [String]
hc2isaNames)
      , (BaseSig
Main_thy, IsaSets -> Set String
consts IsaSets
mainS), (BaseSig
HOLCF_thy, IsaSets -> Set String
consts IsaSets
holcfS)]}

getAltTokenList :: String -> Int -> Id -> BaseSig -> [Token]
getAltTokenList :: String -> Int -> Id -> BaseSig -> [Token]
getAltTokenList newPlace :: String
newPlace over :: Int
over i :: Id
i@(Id ms :: [Token]
ms cs :: [Id]
cs qs :: Range
qs) thy :: BaseSig
thy = let
    (fs :: [Token]
fs, ps :: [Token]
ps) = [Token] -> ([Token], [Token])
splitMixToken [Token]
ms
    nonPlaces :: [Token]
nonPlaces = (Token -> Bool) -> [Token] -> [Token]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Token -> Bool) -> Token -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> Bool
isPlace) [Token]
fs
    constSet :: Set String
constSet = Set String -> BaseSig -> Map BaseSig (Set String) -> Set String
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set String
forall a. Set a
Set.empty BaseSig
thy (Map BaseSig (Set String) -> Set String)
-> Map BaseSig (Set String) -> Set String
forall a b. (a -> b) -> a -> b
$ IsaPreludes -> Map BaseSig (Set String)
preConsts IsaPreludes
isaPrelude
    over2 :: Bool
over2 = [Token] -> Bool
forall a. [a] -> Bool
isSingle [Token]
nonPlaces Bool -> Bool -> Bool
&& String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Token -> String
tokStr (Token -> String) -> Token -> String
forall a b. (a -> b) -> a -> b
$ [Token] -> Token
forall a. [a] -> a
head [Token]
nonPlaces)
            Set String
constSet Bool -> Bool -> Bool
|| String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Id -> String
forall a. Show a => a -> String
show Id
i) Set String
constSet
    o1 :: Int
o1 = if Bool
over2 Bool -> Bool -> Bool
&& Int
over Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then Int
over Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 else Int
over
    newFs :: [Token]
newFs =
      let (fps :: [Token]
fps, rts :: [Token]
rts) = (Token -> Bool) -> [Token] -> ([Token], [Token])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Token -> Bool
isPlace [Token]
fs in case [Token]
rts of
        hd :: Token
hd : tl :: [Token]
tl | Int
o1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 -> [Token]
fps [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ String -> Token
mkSimpleId (Token -> String
tokStr Token
hd String -> String -> String
forall a. [a] -> [a] -> [a]
++
            if Int
o1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 3 then Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
o1 '\'' else '_' Char -> String -> String
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
o1)
                  Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
tl
        _ -> [Token]
fs
    in String -> Id -> [Token]
getTokenList String
newPlace (Id -> [Token]) -> Id -> [Token]
forall a b. (a -> b) -> a -> b
$ [Token] -> [Id] -> Range -> Id
Id ([Token]
newFs [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token]
ps) [Id]
cs Range
qs

toAltSyntax :: Bool -> Int -> GlobalAnnos -> Int -> Id -> BaseSig
            -> Set.Set String -> Maybe AltSyntax
toAltSyntax :: Bool
-> Int
-> GlobalAnnos
-> Int
-> Id
-> BaseSig
-> Set String
-> Maybe AltSyntax
toAltSyntax prd :: Bool
prd over :: Int
over ga :: GlobalAnnos
ga n :: Int
n i :: Id
i thy :: BaseSig
thy toks :: Set String
toks = let
    (precMap :: Map Id Int
precMap, mx :: Int
mx) = Rel Id -> (Map Id Int, Int)
forall a. Ord a => Rel a -> (Map a Int, Int)
Rel.toPrecMap (Rel Id -> (Map Id Int, Int)) -> Rel Id -> (Map Id Int, Int)
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> Rel Id
prec_annos GlobalAnnos
ga
    minPrec :: Int
minPrec = if Bool
prd then 42 else 52
    adjustPrec :: Int -> Int
adjustPrec p :: Int
p = 2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
p Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
minPrec
    br :: String
br = "/ "
    newPlace :: String
newPlace = String
br String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_"
    minL :: [Int]
minL = Int -> Int -> [Int]
forall a. Int -> a -> [a]
replicate Int
n Int
lowPrio
    minL1 :: [Int]
minL1 = [Int] -> [Int]
forall a. [a] -> [a]
tail [Int]
minL
    minL2 :: [Int]
minL2 = [Int] -> [Int]
forall a. [a] -> [a]
tail [Int]
minL1
    ni :: Int
ni = Id -> Int
placeCount Id
i
    atoks :: [Token]
atoks@(hd :: Token
hd : tl :: [Token]
tl) = String -> Int -> Id -> BaseSig -> [Token]
getAltTokenList String
newPlace Int
over Id
i BaseSig
thy
    compoundToks :: [String]
compoundToks = (Char -> String) -> String -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Char -> String -> String
forall a. a -> [a] -> [a]
: []) ",[]{}"
    convert :: Token -> String
convert Token { tokStr :: Token -> String
tokStr = String
s } =
      if String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
s ([String] -> Bool) -> [String] -> Bool
forall a b. (a -> b) -> a -> b
$ String
newPlace String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
compoundToks then String
s else String
br String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
quote String
s
    tts :: String
tts = (Token -> String) -> [Token] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Token -> String
convert [Token]
tl
    ht :: String
ht = let chd :: String
chd = Token -> String
convert Token
hd in
      if String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
br String
chd then Int -> String -> String
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
br) String
chd else String
chd
    ts :: String
ts = String
ht String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tts
    (precList :: [Int]
precList, erg :: Int
erg)
      | Id -> Bool
isInfix Id
i = case Id -> Map Id Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i Map Id Int
precMap of
        Just p :: Int
p -> let
            q :: Int
q = Int -> Int
adjustPrec Int
p
            (l :: Int
l, r :: Int
r) = case Id -> Map Id AssocEither -> Maybe AssocEither
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i (Map Id AssocEither -> Maybe AssocEither)
-> Map Id AssocEither -> Maybe AssocEither
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> Map Id AssocEither
assoc_annos GlobalAnnos
ga of
                 Nothing -> (Int
q Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1, Int
q Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
                 Just ALeft -> (Int
q, Int
q Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
                 Just ARight -> (Int
q Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1, Int
q)
            in (Int
l Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
minL2 [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int
r], Int
q)
        Nothing -> let q :: Int
q = Int -> Int
adjustPrec (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ Int
mx Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 in (Int
q Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
minL2 [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int
q], Int
minPrec)
      | Id -> Bool
begPlace Id
i = let q :: Int
q = Int -> Int
adjustPrec (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ Int
mx Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 3 in (Int
q Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
minL1 , Int
q)
      | Id -> Bool
endPlace Id
i = let q :: Int
q = Int -> Int
adjustPrec (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ Int
mx Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 2 in ([Int]
minL1 [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int
q], Int
q)
      | Bool
otherwise = ([Int]
minL, Int
maxPrio Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1)
    in if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0 Bool -> Bool -> Bool
|| Int
ni Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1 Bool -> Bool -> Bool
&& Int
ni Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
n
           Bool -> Bool -> Bool
|| (Token -> Bool) -> [Token] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((String -> Set String -> Bool) -> Set String -> String -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Set String
toks (String -> Bool) -> (Token -> String) -> Token -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> String
tokStr) [Token]
atoks then Maybe AltSyntax
forall a. Maybe a
Nothing
       else AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then String -> [Int] -> Int -> AltSyntax
AltSyntax String
ts [] Int
maxPrio
       else if Id -> Bool
isMixfix Id
i then String -> [Int] -> Int -> AltSyntax
AltSyntax
                ('(' Char -> String -> String
forall a. a -> [a] -> [a]
: String
ts String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")") [Int]
precList Int
erg
       else String -> [Int] -> Int -> AltSyntax
AltSyntax
            (String
ts String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/'(" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                   [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Int -> String -> [String]
forall a. Int -> a -> [a]
replicate (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) "_,/ ")
                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_')") (Int -> Int -> [Int]
forall a. Int -> a -> [a]
replicate Int
n 3) (Int -> AltSyntax) -> Int -> AltSyntax
forall a b. (a -> b) -> a -> b
$ Int
maxPrio Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1

quote :: String -> String
quote :: String -> String
quote l :: String
l = case String
l of
    [] -> String
l
    c :: Char
c : r :: String
r -> (if Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
c "_/'()" then '\'' Char -> String -> String
forall a. a -> [a] -> [a]
: [Char
c]
              else if Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
c "\\\"" then '\\' Char -> String -> String
forall a. a -> [a] -> [a]
: [Char
c] else [Char
c]) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
quote String
r

showIsaT1 :: (String -> String) -> Id -> String
showIsaT1 :: (String -> String) -> Id -> String
showIsaT1 tr :: String -> String
tr ide :: Id
ide = let
    str :: String
str = String -> String
tr (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Id -> String
forall a. Show a => a -> String
show Id
ide
    in if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
str then String -> String
forall a. HasCallStack => String -> a
error "showIsaT1" else if
       Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (String -> Char
forall a. [a] -> a
last String
str) "_" then String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ "X" else String
str

showIsaConstT :: Id -> BaseSig -> String
showIsaConstT :: Id -> BaseSig -> String
showIsaConstT ide :: Id
ide thy :: BaseSig
thy = (String -> String) -> Id -> String
showIsaT1 (BaseSig -> String -> String
transConstStringT BaseSig
thy) Id
ide

-- also pass number of arguments
mkIsaConstT :: Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> Set.Set String
            -> VName
mkIsaConstT :: Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> Set String -> VName
mkIsaConstT = Int
-> (Id -> BaseSig -> String)
-> Bool
-> GlobalAnnos
-> Int
-> Id
-> BaseSig
-> Set String
-> VName
mkIsaConstVName 0 Id -> BaseSig -> String
showIsaConstT

mkIsaConstVName :: Int -> (Id -> BaseSig -> String) -> Bool -> GlobalAnnos
                -> Int -> Id -> BaseSig -> Set.Set String -> VName
mkIsaConstVName :: Int
-> (Id -> BaseSig -> String)
-> Bool
-> GlobalAnnos
-> Int
-> Id
-> BaseSig
-> Set String
-> VName
mkIsaConstVName over :: Int
over f :: Id -> BaseSig -> String
f prd :: Bool
prd ga :: GlobalAnnos
ga n :: Int
n ide :: Id
ide thy :: BaseSig
thy toks :: Set String
toks =
  let s :: String
s = Id -> BaseSig -> String
f Id
ide BaseSig
thy
      a :: Maybe AltSyntax
a = Bool
-> Int
-> GlobalAnnos
-> Int
-> Id
-> BaseSig
-> Set String
-> Maybe AltSyntax
toAltSyntax Bool
prd Int
over GlobalAnnos
ga Int
n Id
ide BaseSig
thy Set String
toks
 in if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 Bool -> Bool -> Bool
&& case Maybe AltSyntax
a of
      Just (AltSyntax as :: String
as [] _) -> String
as String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
s
      _ -> Bool
False then VName :: String -> Maybe AltSyntax -> VName
VName { new :: String
new = String
s, altSyn :: Maybe AltSyntax
altSyn = Maybe AltSyntax
forall a. Maybe a
Nothing }
    else VName :: String -> Maybe AltSyntax -> VName
VName
  { new :: String
new = (if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0 Bool -> Bool -> Bool
|| Id -> Bool
isMixfix Id
ide Bool -> Bool -> Bool
|| String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= Id -> String
forall a. Show a => a -> String
show Id
ide then String -> String
forall a. a -> a
id else ("X_" String -> String -> String
forall a. [a] -> [a] -> [a]
++)) String
s
  , altSyn :: Maybe AltSyntax
altSyn = Maybe AltSyntax
a }

showIsaTypeT :: Id -> BaseSig -> String
showIsaTypeT :: Id -> BaseSig -> String
showIsaTypeT ide :: Id
ide thy :: BaseSig
thy = (String -> String) -> Id -> String
showIsaT1 (BaseSig -> String -> String
transTypeStringT BaseSig
thy) Id
ide

-- | add a number for overloading
showIsaConstIT :: Id -> Int -> BaseSig -> String
showIsaConstIT :: Id -> Int -> BaseSig -> String
showIsaConstIT ide :: Id
ide i :: Int
i thy :: BaseSig
thy = Id -> BaseSig -> String
showIsaConstT Id
ide BaseSig
thy String -> String -> String
forall a. [a] -> [a] -> [a]
++ "X" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i

mkIsaConstIT :: Bool -> GlobalAnnos -> Int -> Id -> Int -> BaseSig
             -> Set.Set String -> VName
mkIsaConstIT :: Bool
-> GlobalAnnos
-> Int
-> Id
-> Int
-> BaseSig
-> Set String
-> VName
mkIsaConstIT prd :: Bool
prd ga :: GlobalAnnos
ga n :: Int
n ide :: Id
ide i :: Int
i =
    Int
-> (Id -> BaseSig -> String)
-> Bool
-> GlobalAnnos
-> Int
-> Id
-> BaseSig
-> Set String
-> VName
mkIsaConstVName Int
i (Id -> Int -> BaseSig -> String
`showIsaConstIT` Int
i) Bool
prd GlobalAnnos
ga Int
n Id
ide

{- | get the tokens of the alternative syntax that should not be used
     as variables -}
getConstIsaToks :: Id -> Int -> BaseSig -> Set.Set String
getConstIsaToks :: Id -> Int -> BaseSig -> Set String
getConstIsaToks ide :: Id
ide i :: Int
i thy :: BaseSig
thy = if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 2 then
   Set String -> Set String -> Set String
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Id -> Int -> BaseSig -> Set String
getConstIsaToksAux Id
ide 0 BaseSig
thy) (Id -> Int -> BaseSig -> Set String
getConstIsaToksAux Id
ide 1 BaseSig
thy)
   else Id -> Int -> BaseSig -> Set String
getConstIsaToksAux Id
ide Int
i BaseSig
thy

getConstIsaToksAux :: Id -> Int -> BaseSig -> Set.Set String
getConstIsaToksAux :: Id -> Int -> BaseSig -> Set String
getConstIsaToksAux ide :: Id
ide i :: Int
i =
   (Token -> Set String -> Set String)
-> Set String -> [Token] -> Set String
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert (String -> Set String -> Set String)
-> (Token -> String) -> Token -> Set String -> Set String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> String
tokStr)
             Set String
forall a. Set a
Set.empty ([Token] -> Set String)
-> (BaseSig -> [Token]) -> BaseSig -> Set String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Int -> Id -> BaseSig -> [Token]
getAltTokenList "" Int
i Id
ide

transIsaInternalName :: String -> String
transIsaInternalName :: String -> String
transIsaInternalName s :: String
s = if String -> Char
forall a. [a] -> a
last String
s Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '_' then String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "X" else String
s

transIsaStringT :: Map.Map BaseSig (Set.Set String) -> BaseSig
                -> String -> String
transIsaStringT :: Map BaseSig (Set String) -> BaseSig -> String -> String
transIsaStringT m :: Map BaseSig (Set String)
m i :: BaseSig
i s :: String
s = let t :: String
t = Bool -> String -> String
transStringAux Bool
False String
s in
  String -> String
transIsaInternalName (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ if String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member String
t
    (Set String -> Bool) -> Set String -> Bool
forall a b. (a -> b) -> a -> b
$ Set String -> Maybe (Set String) -> Set String
forall a. a -> Maybe a -> a
fromMaybe (String -> Set String
forall a. HasCallStack => String -> a
error "Isabelle.transIsaStringT") (Maybe (Set String) -> Set String)
-> Maybe (Set String) -> Set String
forall a b. (a -> b) -> a -> b
$ BaseSig -> Map BaseSig (Set String) -> Maybe (Set String)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup BaseSig
i Map BaseSig (Set String)
m
  then Map BaseSig (Set String) -> BaseSig -> String -> String
transIsaStringT Map BaseSig (Set String)
m BaseSig
i (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ '_' Char -> String -> String
forall a. a -> [a] -> [a]
: String
s else String
t

transConstStringT :: BaseSig -> String -> String
transConstStringT :: BaseSig -> String -> String
transConstStringT = Map BaseSig (Set String) -> BaseSig -> String -> String
transIsaStringT (Map BaseSig (Set String) -> BaseSig -> String -> String)
-> Map BaseSig (Set String) -> BaseSig -> String -> String
forall a b. (a -> b) -> a -> b
$ IsaPreludes -> Map BaseSig (Set String)
preConsts IsaPreludes
isaPrelude

transTypeStringT :: BaseSig -> String -> String
transTypeStringT :: BaseSig -> String -> String
transTypeStringT = Map BaseSig (Set String) -> BaseSig -> String -> String
transIsaStringT (Map BaseSig (Set String) -> BaseSig -> String -> String)
-> Map BaseSig (Set String) -> BaseSig -> String -> String
forall a b. (a -> b) -> a -> b
$ IsaPreludes -> Map BaseSig (Set String)
preTypes IsaPreludes
isaPrelude

-- | check for legal alphanumeric Isabelle characters
isIsaChar :: Char -> Bool
isIsaChar :: Char -> Bool
isIsaChar c :: Char
c = Char -> Bool
isAlphaNum Char
c Bool -> Bool -> Bool
&& Char -> Bool
isAscii Char
c Bool -> Bool -> Bool
|| Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
c "_'"

-- | translate to a valid Isabelle string possibly non-injectively
transString :: String -> String
transString :: String -> String
transString = Bool -> String -> String
transStringAux Bool
True

-- | if true don't try to be injective
transStringAux :: Bool -> String -> String
transStringAux :: Bool -> String -> String
transStringAux b :: Bool
b str :: String
str = let
    x :: Char
x = 'X'
    replaceChar1 :: Char -> String
replaceChar1 d :: Char
d | Bool -> Bool
not Bool
b Bool -> Bool -> Bool
&& Char
d Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
x = [Char
x, Char
x]  -- code out existing X!
                   | Bool
b Bool -> Bool -> Bool
&& Char
d Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== ' ' = "_"
                   | Char -> Bool
isIsaChar Char
d = [Char
d]
                   | Bool
otherwise = Char
x Char -> String -> String
forall a. a -> [a] -> [a]
: Char -> String
replaceChar Char
d
    in case String
str of
    "" -> String -> String
forall a. HasCallStack => String -> a
error "transString"
    c :: Char
c : s :: String
s -> let l :: String
l = Char -> String
replaceChar1 Char
c in
             (if Char -> Bool
isDigit Char
c Bool -> Bool -> Bool
|| Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
c "_'" then [Char
x, Char
c]
             else String
l) String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char -> String) -> String -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
replaceChar1
        (if Bool
b then String -> String -> String -> String
forall a. Eq a => [a] -> [a] -> [a] -> [a]
replace "' '" "'Space'" String
s else String
s)

-- | injective replacement of special characters
replaceChar :: Char -> String
-- <http://www.htmlhelp.com/reference/charset/>
replaceChar :: Char -> String
replaceChar c :: Char
c = if Char -> Bool
isIsaChar Char
c then [Char
c] else let n :: Int
n = Char -> Int
ord Char
c in
    if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 32 Bool -> Bool -> Bool
|| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 127 Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 160 Bool -> Bool -> Bool
|| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 255 then "Slash_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
    else Char -> String
lookupCharMap Char
c